proposition: Theorem rank2_max_pdiv gT p q (G : {group gT}) : solvable G -> odd #|G| -> 'r_p(G) <= 2 -> q \in \pi(G / 'O_p^'(G)) -> q <= p.
proof: Proof. rewrite mem_primes => solG oddG rG /and3P[pr_q _ /= q_dv_G]. without loss Gp'1: gT G solG oddG rG q_dv_G / 'O_p^'(G) = 1. move/(_ _ (G / 'O_p^'(G))%G); rewrite quotient_odd ?quotient_sol //. rewrite trivg_pcore_quotient -(card_isog (quotient1_isog _)). by rewrite p_rank_p'quotient ?pcore_pgroup ?gFnorm //; apply. set R := 'O_p(G); have pR: p.-group R := pcore_pgroup p G. have [sRG nRG] := andP (pcore_normal p G : R <| G). have oddR: odd #|R| := oddSg sRG oddG. have rR: 'r(R) <= 2 by rewrite (rank_pgroup pR) (leq_trans _ rG) ?p_rankS. rewrite leq_eqVlt -implyNb; apply/implyP=> p'q. have [|//] := pi_Aut_rank2_pgroup pR oddR rR _ p'q; rewrite eq_sym in p'q. apply: (piSg (Aut_conj_aut _ G)); apply: contraLR q_dv_G. rewrite -p'groupEpi -p'natE // Gp'1 -(card_isog (quotient1_isog _)) /pgroup. rewrite -(card_isog (first_isog_loc _ _)) // -!pgroupE ker_conj_aut /= -/R. set C := 'C_G(R); rewrite pquotient_pgroup ?normsI ?norms_cent ?normG //= -/C. suffices sCR: C \subset R by rewrite (pgroupS sCR (pi_pnat pR _)). by rewrite /C /R -(Fitting_eq_pcore _) ?cent_sub_Fitting. 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)