proposition: Lemma Fitting_sub_FTsupp : 'F(M)^# \subset 'A(M).
proof: Proof. pose pi := \pi(M`_\F); have nilF := Fitting_nil M. have [U defF]: {U : {group gT} | M`_\F \x U = 'F(M)}. have hallH := pHall_subl (Fcore_sub_Fitting M) (gFsub _ _) (Fcore_Hall M). exists 'O_pi^'('F(M))%G; rewrite (nilpotent_Hall_pcore nilF hallH). exact: nilpotent_pcoreC. apply/subsetP=> xy /setD1P[ntxy Fxy]; apply/bigcupP. have [x [y [Hx Vy Dxy _]]] := mem_dprod defF Fxy. have [z [ntz Hz czxy]]: exists z, [/\ z != 1%g, z \in M`_\F & x \in 'C[z]]. have [-> | ntx] := eqVneq x 1%g; last by exists x; rewrite ?cent1id. by have /trivgPn[z ntz] := mmax_Fcore_neq1 maxM; exists z; rewrite ?group1. exists z; first by rewrite !inE ntz (subsetP (Fcore_sub_FTcore maxM)). rewrite 3!inE ntxy {2}Dxy groupMl //= andbC (subsetP _ y Vy) //=; last first. by rewrite sub_cent1 (subsetP _ _ Hz) // centsC; have [] := dprodP defF. rewrite -FTtype_Pmax // (subsetP _ xy Fxy) //. case MtypeP: (M \in _); last exact: gFsub. by have [_ _ _ ->] := Fitting_structure maxM. 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 frobenius) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14 BGsection15)