proposition: Theorem Malpha_quo_rank2 : 'r(M / M`_\alpha) <= 2.
proof: Proof. have [p p_pr ->] := rank_witness (M / M`_\alpha). have [P sylP] := Sylow_exists p M; have [sPM pP _] := and3P sylP. have nMaP := subset_trans sPM (normal_norm nsMaM). rewrite -(rank_Sylow (quotient_pHall nMaP sylP)) /= leqNgt. have [a_p | a'p] := boolP (p \in \alpha(M)). by rewrite quotientS1 ?rank1 ?(sub_Hall_pcore Malpha_Hall) ?(pi_pgroup pP). rewrite -(isog_rank (quotient_isog _ _)) ?coprime_TIg ?(rank_Sylow sylP) //. exact: pnat_coprime aMa (pi_pnat pP _). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9)