proposition: Lemma lcoset_in_rcoset_impl_normal {X : gr} (N : subgr X) : lcoset_in_rcoset N -> isnormalsubgr N.
proof: Proof. intros lcinrc. unfold isnormalsubgr. intros g n1. refine (@transportb _ (fun x => N x) _ _ _ _). { etrans. { apply maponpaths_2, (lcoset_in_rcoset_equation lcinrc). } etrans. { apply assocax. } etrans. { apply maponpaths, grrinvax. } apply runax. } apply lcoset_in_rcoset_property. Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids