proposition: Lemma normsRl A G B : A \subset G -> A \subset 'N([~: G, B]).
proof: Proof. by move=> sAG; apply: subset_trans (commg_norml G B). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)