proposition: Theorem rank2_min_p_complement gT (G : {group gT}) (p := pdiv #|G|) : solvable G -> odd #|G| -> 'r_p(G) <= 2 -> p^'.-Hall(G) 'O_p^'(G).
proof: Proof. move=> solG oddG rG; rewrite /pHall pcore_pgroup pcore_sub pnatNK /=. rewrite -card_quotient ?gFnorm //; apply/pgroupP=> q q_pr q_dv_Gb. rewrite inE /= eqn_leq (rank2_max_pdiv _ _ rG) ?mem_primes ?q_pr ?cardG_gt0 //. by rewrite pdiv_min_dvd ?prime_gt1 ?(dvdn_trans q_dv_Gb) ?dvdn_quotient. 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)