proposition: Lemma commg_subl G H : ([~: G, H] \subset G) = (H \subset 'N(G)).
proof: Proof. by rewrite commGC commg_subr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)