proposition: Theorem cent_rank3_Uniqueness K : 'r(K) >= 2 -> 'r('C(K)) >= 3 -> K \in 'U.
proof: Proof. move=> Kge2 CKge3; have cCK_K: K \subset 'C('C(K)) by rewrite centsC. apply: cent_uniq_Uniqueness cCK_K _ => //. apply: rank3_Uniqueness (mFT_cent_proper _) CKge3. by rewrite -rank_gt0 ltnW. 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)