proposition: Lemma any_rank3_Fitting_Uniqueness p M P : M \in 'M -> 'r_p('F(M)) >= 3 -> p.-group P -> 'r(P) >= 3 -> P \in 'U.
proof: Proof. move=> maxM FMge3 pP; rewrite (rank_pgroup pP) => /p_rank_geP[B]. case/pnElemP=> sBP abelB dimB3; have [pB cBB _] := and3P abelB. have CBge3: 'r_p('C(B)) >= 3 by rewrite -dimB3 -(p_rank_abelem abelB) p_rankS. have ncycB: ~~ cyclic B by rewrite (abelem_cyclic abelB) dimB3. apply: {P pP}uniq_mmaxS sBP (mFT_pgroup_proper pP) _. case/orP: (orbN (p.-group 'F(M))) => [pFM | pFM']. have [P sylP sFP] := Sylow_superset (Fitting_sub _) pFM. have pP := pHall_pgroup sylP. have [|A SCN_A]:= rank3_SCN3 pP (mFT_odd _). by rewrite (leq_trans FMge3) ?p_rankS. have [_ _ uA] := SCN_Fitting_Uniqueness maxM pFM sylP FMge3 SCN_A. case/setIdP: SCN_A => SCN_A dimA3; case: (setIdP SCN_A); case/andP=> sAP _ _. have cAA := SCN_abelian SCN_A; have pA := pgroupS sAP pP. exact: (any_cent_rank3_Uniquness cAA pA). have [A0 EpA0 A0ge3] := p_rank_pmaxElem_exists FMge3. have uA := non_pcore_Fitting_Uniqueness maxM pFM' EpA0 A0ge3. case/pmaxElemP: EpA0; case/setIdP=> _ abelA0 _. have [pA0 cA0A0 _] := and3P abelA0; rewrite -rank_pgroup // in A0ge3. rewrite (any_cent_rank3_Uniquness _ pA0) // (cent_uniq_Uniqueness uA) 1?ltnW //. by rewrite centsC subsetIr. 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)