proposition: Proposition coprime_Hall_exists A G : A \subset 'N(G) -> coprime #|G| #|A| -> solvable G -> exists2 H : {group gT}, pi.-Hall(G) H & A \subset 'N(H).
proof: Proof. move=> nGA coGA solG; have [H hallH] := Hall_exists pi solG. have sG_AG: G \subset A <*> G by rewrite joing_subr. have nG_AG: A <*> G \subset 'N(G) by rewrite join_subG nGA normG. pose N := 'N_(A <*> G)(H)%G. have nGN: N \subset 'N(G) by rewrite subIset ?nG_AG. have nGN_N: G :&: N <| N by rewrite /(_ <| N) subsetIr normsI ?normG. have NG_AG: G * N = A <*> G. by apply: Hall_Frattini_arg hallH => //; apply/andP. have iGN_A: #|N| %/ #|G :&: N| = #|A|. rewrite setIC divgI -card_quotient // -quotientMidl NG_AG. rewrite card_quotient -?divgS //= norm_joinEl //. by rewrite coprime_cardMg 1?coprime_sym // mulnK. have hallGN: Hall N (G :&: N). by rewrite /Hall -divgS subsetIr //= iGN_A (coprimeSg _ coGA) ?subsetIl. case/splitsP: {hallGN nGN_N}(SchurZassenhaus_split hallGN nGN_N) => B. case/complP=> trBGN defN. have{trBGN iGN_A} oBA: #|B| = #|A|. by rewrite -iGN_A -{1}defN (TI_cardMg trBGN) mulKn. have sBN: B \subset N by rewrite -defN mulG_subr. case: (SchurZassenhaus_trans_sol solG nGA _ coGA oBA) => [|x Gx defB]. by rewrite -(normC nGA) -norm_joinEl // -NG_AG -(mul1g B) mulgSS ?sub1G. exists (H :^ x^-1)%G; first by rewrite pHallJ ?groupV. apply/subsetP=> y Ay; have: y ^ x \in B by rewrite defB memJ_conjg. move/(subsetP sBN)=> /setIP[_ /normP nHyx]. by apply/normP; rewrite -conjsgM conjgCV invgK conjsgM nHyx. 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)