proposition: Lemma normal_lcoset_in_rcoset {X : gr} (N : normalsubgr X) : lcoset_in_rcoset N.
proof: Proof. unfold normalsubgr in N. induction N as [N normalprop]. simpl. unfold lcoset_in_rcoset. intros g n1. use tpair. - exact (tpair _ (g * (pr1 n1) * (grinv X g)) (normalprop g n1)). - simpl. rewrite (assocax _ _ _ g). rewrite (grlinvax X _). rewrite (runax X). reflexivity. Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids