proposition: Theorem rank2_max_pcore_Sylow gT (G : {group gT}) (p := max_pdiv #|G|) : odd #|G| -> solvable G -> 'r('F(G)) <= 2 -> p.-Sylow(G) 'O_p(G).
proof: Proof. move=> oddG solG Fle2; pose pi := [pred q | p <= q]. rewrite pHallE pcore_sub eqn_leq -{1}(part_pnat_id (pcore_pgroup _ _)). rewrite dvdn_leq ?partn_dvd ?cardSg ?pcore_sub // /=. rewrite (@eq_in_partn _ pi) => [|q piGq]; last first. by rewrite !inE eqn_leq; apply: andb_idl => le_q_p; apply: max_pdiv_max. rewrite -(card_Hall (rank2_ge_pcore_Hall p oddG solG Fle2)) -/pi. rewrite subset_leq_card // pcore_max ?pcore_normal //. apply: sub_in_pnat (pcore_pgroup _ _) => q /(piSg (pcore_sub _ _))-piGq. by rewrite !inE eqn_leq max_pdiv_max. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)