proposition: Lemma exceptional_pmaxElem : A \in 'E*_p(G).
proof: Proof. have [_ _ dimA]:= pnElemP Ep2A. apply/pmaxElemP; split=> [|E EpE sAE]; first by rewrite !inE subsetT. have [//|ltAE]: A :=: E \/ A \proper E := eqVproper sAE. have [_ abelE] := pElemP EpE; have [pE cEE _] := and3P abelE. suffices: logn p #|E| <= 'r_p(M) by rewrite leqNgt rM -dimA properG_ltn_log. by rewrite logn_le_p_rank // inE (subset_trans cEE) ?(subset_trans (centS sAE)). 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 BGsection10)