proposition: Theorem rank3_Uniqueness K : K \proper G -> 'r(K) >= 3 -> K \in 'U.
proof: Proof. move=> prK /rank_geP[B /nElemP[p /pnElemP[sBK abelB dimB3]]]. have [pB cBB _] := and3P abelB. suffices: B \in 'U by apply: uniq_mmaxS. have [P sylP sBP] := Sylow_superset (subsetT _) pB. have pP := pHall_pgroup sylP. have [|A SCN3_A] := rank3_SCN3 pP (mFT_odd _). by rewrite -dimB3 -(rank_abelem abelB) (rank_pgroup pB) p_rankS. have [SCN_A Age3] := setIdP SCN3_A. have: A \in 'SCN_3[p] by apply/bigcupP; exists P; rewrite // inE. move/SCN_3_Uniqueness=> uA; have cAA := SCN_abelian SCN_A. case/setIdP: SCN_A; case/andP=> sAP _ _; have pA := pgroupS sAP pP. apply: any_cent_rank3_Uniquness uA pB _ _ => //. by rewrite (abelem_cyclic abelB) dimB3. by rewrite -dimB3 -p_rank_abelem ?p_rankS. 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)