proposition: Lemma coprime_cent_mulG A G H : A \subset 'N(G) -> A \subset 'N(H) -> G \subset 'N(H) -> coprime #|H| #|A| -> solvable H -> 'C_(H * G)(A) = 'C_H(A) * 'C_G(A).
proof: Proof. move=> nHA nGA nHG coHA solH; rewrite -norm_joinEr //. have nsHG: H <| H <*> G by rewrite /normal joing_subl join_subG normG. rewrite -{2}(setIidPr (normal_sub nsHG)) setIAC. rewrite group_modr ?setSI ?joing_subr //=; symmetry; apply/setIidPl. rewrite -quotientSK ?subIset 1?normal_norm //. by rewrite !coprime_norm_quotient_cent ?normsY //= norm_joinEr ?quotientMidl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)