proposition: Theorem nonmaxElem2_Uniqueness p A : A \in 'E_p^2(G) :\: 'E*_p(G) -> A \in 'U.
proof: Proof. case/setDP=> EpA nmaxA; have [_ abelA dimA2]:= pnElemP EpA. case/setIdP: EpA => EpA _; have [pA _] := andP abelA. apply: cent_rank3_Uniqueness; first by rewrite -dimA2 -(rank_abelem abelA). have [E maxE sAE] := pmaxElem_exists EpA. have [/pElemP[_ abelE _]] := pmaxElemP maxE; have [pE cEE _] := and3P abelE. have: 'r(E) <= 'r('C(A)) by rewrite rankS // (subset_trans cEE) ?centS. apply: leq_trans; rewrite (rank_abelem abelE) -dimA2 properG_ltn_log //. by rewrite properEneq; case: eqP maxE nmaxA => // => /group_inj-> ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div fintype path) mathcomp(finset prime fingroup action automorphism quotient cyclic) mathcomp(gproduct gfunctor pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection8)