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