proposition: Theorem rank2_ge_pcore_Hall gT m (G : {group gT}) (pi := [pred p | p >= m]) : odd #|G| -> solvable G -> 'r('F(G)) <= 2 -> pi.-Hall(G) 'O_pi(G).
proof: Proof. elim: {G}_.+1 {-2}G (ltnSn #|G|) => // n IHn G. rewrite ltnS => leGn oddG solG Fle2; pose p := pdiv #|G|. have [defGpi | not_pi_G] := eqVneq 'O_pi(G) G. by rewrite /pHall pcore_sub pcore_pgroup defGpi indexgg. have pi'_p: (p \in pi^'). apply: contra not_pi_G => pi_p; rewrite eqEsubset pcore_sub pcore_max //. apply/pgroupP=> q q_pr qG; apply: leq_trans pi_p _. by rewrite pdiv_min_dvd ?prime_gt1. pose Gp' := 'O_p^'(G); have sGp'G: Gp' \subset G := pcore_sub _ _. have hallGp'pi: pi.-Hall(Gp') 'O_pi(Gp'). apply: IHn; rewrite ?(oddSg sGp'G) ?(solvableS sGp'G) //; last first. by apply: leq_trans (rankS _) Fle2; rewrite /= Fitting_pcore pcore_sub. apply: leq_trans (proper_card _) leGn. rewrite properEneq pcore_sub andbT; apply/eqP=> defG. suff: p \in p^' by case/eqnP. have p'G: p^'.-group G by rewrite -defG pcore_pgroup. rewrite (pgroupP p'G) ?pdiv_dvd ?pdiv_prime // cardG_gt1. by apply: contra not_pi_G; move/eqP->; rewrite (trivgP (pcore_sub _ _)). have defGp'pi: 'O_pi(Gp') = 'O_pi(G). rewrite -pcoreI; apply: eq_pcore => q; apply: andb_idr. by apply: contraL => /=; move/eqnP->. have hallGp': p^'.-Hall(G) Gp' by rewrite rank2_min_p'core_Hall. rewrite pHallE pcore_sub /= -defGp'pi (card_Hall hallGp'pi) (card_Hall hallGp'). by rewrite partn_part // => q; apply: contraL => /=; move/eqnP->. 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)