proposition: Lemma Fitting_max G H : H <| G -> nilpotent H -> H \subset 'F(G).
proof: Proof. move=> nsHG nilH; rewrite -(Sylow_gen H) gen_subG. apply/bigcupsP=> P /SylowP[p _ sylP]. case Gp: (p \in \pi(G)); last first. rewrite card1_trivg ?sub1G // (card_Hall sylP). rewrite part_p'nat // (pnat_dvd (cardSg (normal_sub nsHG))) //. by rewrite /pnat cardG_gt0 all_predC has_pred1 Gp. rewrite {P sylP}(nilpotent_Hall_pcore nilH sylP). rewrite -(bigdprodWY (erefl 'F(G))) sub_gen //. rewrite -(filter_pi_of (ltnSn _)) big_filter big_mkord. apply: (bigcup_max (Sub p _)) => //= [|_]. by have:= Gp; rewrite ltnS mem_primes => /and3P[_ ntG /dvdn_leq->]. by rewrite pcore_max ?pcore_pgroup ?gFnormal_trans. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)