proposition: Lemma in_same_coset_isbinophrel {X : gr} (N : normalsubgr X) : isbinophrel (in_same_left_coset_eqrel N).
proof: 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 _ (grinv X c) _ _). rewrite (!assocax _ c _ _). rewrite (grrinvax _). rewrite (lunax _). rewrite (!assocax _ a _ _). apply maponpaths_2. exact (pr2 ab_same_lcoset). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids