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