proposition: Proposition Fitting_stab_chief : 'F(G') \subset H.
proof: Proof. apply/bigcapsP=> [[U V] /= chiefUV]. have minUV: minnormal (U / V) (G / V) := chief_factor_minnormal chiefUV. have{chiefUV} [/=/maxgroupp/andP[_ nVG] sUG nUG] := and3P chiefUV. have solUV: solvable (U / V) by rewrite quotient_sol // (solvableS sUG). have{solUV minUV}: U / V \subset 'Z('F(G / V)). exact: minnormal_solvable_Fitting_center minUV (quotientS V sUG) solUV. rewrite sub_astabQ gFsub_trans ?(subset_trans sG'G) //=. case/subsetIP=> _; rewrite centsC; apply: subset_trans. by rewrite Fitting_max ?quotient_normal ?quotient_nil ?Fitting_nil. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)