proposition: Lemma commg_norml G A : G \subset 'N([~: G, A]).
proof: Proof. apply/subsetP=> x Gx; rewrite inE -genJ gen_subG. apply/subsetP=> _ /imsetP[_ /imset2P[y z Gy Az ->] ->]. by rewrite -(mulgK [~ x, z] (_ ^ x)) -commMgJ !(mem_commg, groupMl, groupV). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)