proposition: Lemma Fitting_pcore pi G : 'F('O_pi(G)) = 'O_pi('F(G)).
proof: Proof. apply/eqP; rewrite eqEsubset. rewrite (subset_trans _ (pcoreS _ (Fitting_sub _))); last first. by rewrite subsetI Fitting_sub Fitting_max ?Fitting_nil ?gFnormal_trans. rewrite (subset_trans _ (FittingS (pcore_sub _ _))) // subsetI pcore_sub. 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)