proposition: Corollary cent_uniq_Uniqueness K L : L \in 'U -> K \subset 'C(L) -> 'r(K) >= 2 -> K \in 'U.
proof: Proof. move=> uL; have ntL := uniq_mmax_neq1 uL. case/uniq_mmaxP: uL => H uL_H cLK; have [maxH sLH] := mem_uniq_mmax uL_H. case/rank_geP=> B /nElemP[p /pnElemP[sBK abelB /eqP dimB2]]. have scBH: \bigcup_(b in B^#) 'C[b] \subset H. apply/bigcupsP=> b /setIdP[]; rewrite inE -cycle_eq1 => ntb Bb. apply: (sub_uniq_mmax uL_H); last by rewrite /= -cent_cycle mFT_cent_proper. by rewrite sub_cent1 (subsetP cLK) ?(subsetP sBK). have EpB: B \in 'E_p(H). apply/pElemP; split=> //; rewrite -(setD1K (group1 B)) subUset sub1G /=. apply/subsetP=> b Bb; apply: (subsetP scBH). by apply/bigcupP; exists b => //; apply/cent1P. have prK: K \proper G by rewrite (sub_proper_trans cLK) ?mFT_cent_proper. apply: uniq_mmaxS prK (noncyclic_cent1_sub_Uniqueness _ EpB _ _) => //. by rewrite (abelem_cyclic abelB) (eqP dimB2). 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)