proposition: Lemma commMG G H K : H \subset 'N([~: G, K]) -> [~: G * H , K] = [~: G, K] * [~: H, K].
proof: Proof. move=> nRH; apply/eqP; rewrite eqEsubset commMGr andbT. have nRHK: [~: H, K] \subset 'N([~: G, K]) by rewrite comm_subG ?commg_normr. have defM := norm_joinEr nRHK; rewrite -defM gen_subG /=. apply/subsetP=> _ /imset2P[_ z /imset2P[x y Gx Hy ->] Kz ->]. by rewrite commMgJ {}defM mem_mulg ?memJ_norm ?mem_commg // (subsetP nRH). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)