Lemma normal_lcoset_in_rcoset {X : gr} (N : normalsubgr X) : lcoset_in_rcoset N. Proof. unfold normalsubgr in N. induction N as [N normalprop]. simpl. unfold lcoset_in_rcoset. intros g n1. use tpair. - exact (g * pr1 n1 / g ,, normalprop g n1). - simpl. rewrite (assocax _ _ _ g). rewrite (grlinvax X _). rewrite (runax X). reflexivity. Defined.
Require Import UniMath.MoreFoundations.Subtypes.