proposition: Lemma subcent_TImulg K H A : K :&: H = 1 -> A \subset 'N(K) :&: 'N(H) -> 'C_K(A) * 'C_H(A) = 'C_(K * H)(A).
proof: Proof. move=> tiKH /subsetIP[nKA nHA]; apply/eqP. rewrite group_modl ?subsetIr // eqEsubset setSI ?mulSg ?subsetIl //=. apply/subsetP=> _ /setIP[/mulsgP[x y Kx Hy ->] cAxy]. rewrite inE cAxy mem_mulg // inE Kx /=. apply/centP=> z Az; apply/commgP/conjg_fixP. move/commgP/conjg_fixP/(congr1 (divgr K H)): (centP cAxy z Az). by rewrite conjMg !divgrMid ?memJ_norm // (subsetP nKA, subsetP nHA). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)