Lemma in_same_coset_isbinophrel {X : gr} (N : normalsubgr X) : isbinophrel (in_same_left_coset_eqrel N). Proof. unfold isbinophrel. split. - intros a b c. unfold in_same_left_coset_eqrel. simpl. unfold in_same_left_coset. intros ab_same_lcoset. use tpair. + exact (pr1 ab_same_lcoset). + simpl. rewrite (assocax _ c _ _). apply maponpaths. exact (pr2 ab_same_lcoset). - intros a b c. unfold in_same_left_coset_eqrel. simpl. unfold in_same_left_coset. intros ab_same_lcoset. use tpair. + refine (rcoset_in_lcoset_witness _ c (pr1 ab_same_lcoset)); apply normal_rcoset_in_lcoset. + simpl. rewrite (grinvinv _). rewrite (assocax _ a _ _). rewrite (assocax _ (c^-1) _ _). rewrite <- (assocax _ c _ _). rewrite (grrinvax _). rewrite (lunax _). rewrite <- (assocax _ a _ _). apply maponpaths_2. exact (pr2 ab_same_lcoset). Defined.
Require Import UniMath.MoreFoundations.Subtypes.