proposition: Lemma Fcore_max pi H : pi.-Hall(M) H -> H <| M -> nilpotent H -> H \subset M`_\F.
proof: Proof. move=> hallH nsHM nilH; have [sHM pi_H _] := and3P hallH. rewrite -(nilpotent_Fitting nilH) FittingEgen genS //. apply/bigcupsP=> [[p /= _] piHp]; rewrite (bigcup_max 'O_p(H)%G) //. have sylHp := nilpotent_pcore_Hall p nilH. have sylHp_M := subHall_Sylow hallH (pnatPpi pi_H piHp) sylHp. by rewrite (p_Sylow sylHp_M) gFnormal_trans. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center 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)