proposition: Lemma coprime_mulG_setI_norm H G K R : K * R = G -> G \subset 'N(H) -> coprime #|K| #|R| -> (K :&: H) * (R :&: H) = G :&: H.
proof: Proof. move=> defG nHG coKR; apply/eqP; rewrite eqEcard mulG_subG /= -defG. rewrite !setSI ?mulG_subl ?mulG_subr //=. rewrite coprime_cardMg ?(coKR, coprimeSg (subsetIl _ _), coprime_sym) //=. pose pi := \pi(K); have piK: pi.-group K by apply: pgroup_pi. have pi'R: pi^'.-group R by rewrite /pgroup -coprime_pi' /=. have [hallK hallR] := coprime_mulpG_Hall defG piK pi'R. have nsHG: H :&: G <| G by rewrite /normal subsetIr normsI ?normG. rewrite -!(setIC H) defG -(partnC pi (cardG_gt0 _)). rewrite -(card_Hall (Hall_setI_normal nsHG hallR)) /= setICA. rewrite -(card_Hall (Hall_setI_normal nsHG hallK)) /= setICA. by rewrite -defG (setIidPl (mulG_subl _ _)) (setIidPl (mulG_subr _ _)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)