proposition: Lemma commMGr G H K : [~: G, K] * [~: H, K] \subset [~: G * H , K].
proof: Proof. by rewrite mul_subG ?commSg ?(mulG_subl, mulG_subr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)