proposition: Proposition beta_noncyclic_uniq p R : p \in \beta(G) -> p.-group R -> 'r(R) > 1 -> R \in 'U.
proof: Proof. move=> b_p pR rRgt1; have [P sylP sRP] := Sylow_superset (subsetT R) pR. rewrite (rank_pgroup pR) in rRgt1; have [A Ep2A] := p_rank_geP rRgt1. have [sAR abelA dimA] := pnElemP Ep2A; have p_pr := pnElem_prime Ep2A. case: (pickP [pred F in 'E_p(P) | A \proper F]) => [F | maxA]; last first. have [_ nnSyl] := beta_not_narrow b_p; case/pred0Pn: (nnSyl P sylP). exists A; rewrite /= (subsetP (pnElemS p 2 sRP)) //. apply/pmaxElemP; split=> [|F EpF]; first by rewrite inE (subset_trans sAR). by case/eqVproper=> [// | ltAF]; case/andP: (maxA F). case/andP=> /pElemP[_ abelF] ltAF; have [pF cFF _] := and3P abelF. apply: uniq_mmaxS sAR (mFT_pgroup_proper pR) _. have rCAgt2: 'r('C(A)) > 2. rewrite -dimA (leq_trans (properG_ltn_log pF ltAF)) // -(rank_abelem abelF). by rewrite rankS // centsC (subset_trans (proper_sub ltAF)). by apply: cent_rank3_Uniqueness rCAgt2; rewrite (rank_abelem abelA) dimA. 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 BGsection9)