proposition: Theorem Fitting_Uniqueness M : M \in 'M -> 'r('F(M)) >= 3 -> 'F(M)%G \in 'U.
proof: Proof. move=> maxM; have [p _ -> dimF3] := rank_witness 'F(M). have prF: 'F(M) \proper G := sub_mmax_proper maxM (Fitting_sub M). have [pF | npF] := boolP (p.-group 'F(M)). have [P sylP] := Sylow_exists p M; have [sPM pP _] := and3P sylP. have dimP3: 'r_p(P) >= 3. rewrite (p_rank_Sylow sylP) (leq_trans dimF3) //. by rewrite p_rankS ?Fitting_sub. have [A] := rank3_SCN3 pP (mFT_odd _) dimP3. by case/(SCN_Fitting_Uniqueness maxM pF)=> // _ sAF; apply: uniq_mmaxS. case/p_rank_geP: dimF3 => A /setIdP[EpA dimA3]. have [A0 maxA0 sAA0] := @maxgroup_exists _ [pred X in 'E_p('F(M))] _ EpA. have [_ abelA] := pElemP EpA; have pmaxA0: A0 \in 'E*_p('F(M)) by rewrite inE. case/pElemP: (maxgroupp maxA0) => sA0F; case/and3P=> _ cA0A0 _. have dimA0_3: 'r_p(A0) >= 3. by rewrite -(eqP dimA3) -(p_rank_abelem abelA) p_rankS. have:= non_pcore_Fitting_Uniqueness maxM npF pmaxA0 dimA0_3. exact: uniq_mmaxS (subsetIl _ _) prF. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div fintype path) mathcomp(finset prime fingroup automorphism action gproduct gfunctor) mathcomp(center commutator pgroup gseries nilpotent sylow abelian maximal) odd_order(BGsection1 BGsection5 BGsection6 BGsection7)