proposition: Lemma Fitting_group_set G : group_set (Fitting G).
proof: Proof. suffices [F ->]: exists F : {group gT}, Fitting G = F by apply: groupP. rewrite /Fitting; elim: primes (primes_uniq #|G|) => [_|p r IHr] /=. by exists [1 gT]%G; rewrite big_nil. case/andP=> rp /IHr[F defF]; rewrite big_cons defF. suffices{IHr} /and3P[p'F sFG nFG]: p^'.-group F && (F <| G). have nFGp: 'O_p(G) \subset 'N(F) := gFsub_trans _ nFG. have pGp: p.-group('O_p(G)) := pcore_pgroup p G. have{pGp} tiGpF: 'O_p(G) :&: F = 1 by rewrite coprime_TIg ?(pnat_coprime pGp). exists ('O_p(G) <*> F)%G; rewrite dprodEY // (sameP commG1P trivgP) -tiGpF. by rewrite subsetI commg_subl commg_subr (subset_trans sFG) // gFnorm. move/bigdprodWY: defF => <- {F}; elim: r rp => [_|q r IHr] /=. by rewrite big_nil gen0 pgroup1 normal1. rewrite inE eq_sym big_cons -joingE -joing_idr => /norP[qp /IHr {IHr}]. set F := <<_>> => /andP[p'F nsFG]. rewrite norm_joinEl /= -/F; last exact/gFsub_trans/normal_norm. by rewrite pgroupM p'F normalM ?pcore_normal //= (pi_pgroup (pcore_pgroup q G)). 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)