Lemma lcoset_equal_rcoset_impl_normal {X : gr} (N : subgr X) : lcoset_equal_rcoset N → isnormalsubgr N. Proof. intros H. apply lcoset_in_rcoset_impl_normal. exact (pr1 H). Defined.
Require Import UniMath.MoreFoundations.Subtypes.