proposition: Lemma Mho_cprod A B G : A \* B = G -> 'Mho^n(A) \* 'Mho^n(B) = 'Mho^n(G).
proof: Proof. case/cprodP => [[H K -> ->{A B}]] <- cHK; rewrite cprodEY //; last first. by rewrite (subset_trans (subset_trans _ cHK)) ?centS ?Mho_sub. apply/eqP; rewrite -(cent_joinEr cHK) eqEsubset join_subG /=. rewrite !MhoS ?joing_subl ?joing_subr //= cent_joinEr // -genM_join. apply: genS; apply/subsetP=> xypn /imsetP[_ /setIdP[/imset2P[x y Hx Ky ->]]]. move/constt_p_elt; move: (pdiv _) => p <- ->. have cxy: commute x y by red; rewrite -(centsP cHK). rewrite consttM // expgMn; last exact: commuteX2. by rewrite mem_mulg ?Mho_p_elt ?groupX ?p_elt_constt. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)