proposition: Lemma sol_coprime_Sylow_subset A G X : A \subset 'N(G) -> coprime #|G| #|A| -> solvable A -> X \subset G -> p.-group X -> A \subset 'N(X) -> exists P : {group gT}, [/\ p.-Sylow(G) P, A \subset 'N(P) & X \subset P].
proof: Proof. move=> nGA coGA solA sXG pX nXA. pose nAp (Q : {group gT}) := [&& p.-group Q, Q \subset G & A \subset 'N(Q)]. have: nAp X by apply/and3P. case/maxgroup_exists=> R; case/maxgroupP; case/and3P=> pR sRG nRA maxR sXR. have [P sylP sRP]:= Sylow_superset sRG pR. suffices defP: P :=: R by exists P; rewrite sylP defP. case/and3P: sylP => sPG pP _; apply: (nilpotent_sub_norm (pgroup_nil pP)) => //. pose N := 'N_G(R); have{sPG} sPN_N: 'N_P(R) \subset N by apply: setSI. apply: norm_sub_max_pgroup (pgroupS (subsetIl _ _) pP) sPN_N (subsetIr _ _). have nNA: A \subset 'N(N) by rewrite normsI ?norms_norm. have coNA: coprime #|N| #|A| by apply: coprimeSg coGA; rewrite subsetIl. have{solA coNA} [Q sylQ nQA] := sol_coprime_Sylow_exists solA nNA coNA. suffices defQ: Q :=: R by rewrite max_pgroup_Sylow -{2}defQ. apply: maxR; first by apply/and3P; case/and3P: sylQ; rewrite subsetI; case/andP. by apply: normal_sub_max_pgroup (Hall_max sylQ) pR _; rewrite normal_subnorm. 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)