proposition: Lemma sol_coprime_Sylow_exists A G : solvable A -> A \subset 'N(G) -> coprime #|G| #|A| -> exists2 P : {group gT}, p.-Sylow(G) P & A \subset 'N(P).
proof: Proof. move=> solA nGA coGA; pose AG := A <*> G. have nsG_AG: G <| AG by rewrite /normal joing_subr join_subG nGA normG. have [sG_AG nG_AG]:= andP nsG_AG. have [P sylP] := Sylow_exists p G; pose N := 'N_AG(P); pose NG := G :&: N. have nGN: N \subset 'N(G) by rewrite subIset ?nG_AG. have sNG_G: NG \subset G := subsetIl G N. have nsNG_N: NG <| N by rewrite /normal subsetIr normsI ?normG. have defAG: G * N = AG := Frattini_arg nsG_AG sylP. have oA : #|A| = #|N| %/ #|NG|. rewrite /NG setIC divgI -card_quotient // -quotientMidl defAG. rewrite card_quotient -?divgS //= norm_joinEl //. by rewrite coprime_cardMg 1?coprime_sym // mulnK. have: [splits N, over NG]. rewrite SchurZassenhaus_split // /Hall -divgS subsetIr //. by rewrite -oA (coprimeSg sNG_G). case/splitsP=> B; case/complP=> tNG_B defN. have [nPB]: B \subset 'N(P) /\ B \subset AG. by apply/andP; rewrite andbC -subsetI -/N -defN mulG_subr. case/SchurZassenhaus_trans_actsol => // [|x Gx defB]. by rewrite oA -defN TI_cardMg // mulKn. exists (P :^ x^-1)%G; first by rewrite pHallJ ?groupV. by rewrite normJ -sub_conjg -defB. 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)