Lemma lcoset_in_rcoset_impl_normal {X : gr} (N : subgr X) : lcoset_in_rcoset N → isnormalsubgr N. Proof. intros lcinrc. unfold isnormalsubgr. intros g n1. refine (@transportb _ (λ 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.
Require Import UniMath.MoreFoundations.Subtypes.