proposition: Lemma FittingEgen G : 'F(G) = <<\bigcup_(p < #|G|.+1 | (p : nat) \in \pi(G)) 'O_p(G)>>.
proof: Proof. apply/eqP; rewrite eqEsubset gen_subG /=. rewrite -{1}(bigdprodWY (erefl 'F(G))) (big_nth 0) big_mkord genS. by apply/bigcupsP=> p _; rewrite -p_core_Fitting pcore_sub. apply/bigcupsP=> [[i /= lti]] _; set p := nth _ _ i. have pi_p: p \in \pi(G) by rewrite mem_nth. have p_dv_G: p %| #|G| by rewrite mem_primes in pi_p; case/and3P: pi_p. have lepG: p < #|G|.+1 by rewrite ltnS dvdn_leq. by rewrite (bigcup_max (Ordinal lepG)). 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)