proposition: Lemma minnormal_solvable_Fitting_center gT (M G : {group gT}) : minnormal M G -> M \subset G -> solvable M -> M \subset 'Z('F(G)).
proof: Proof. have nZG: 'Z('F(G)) <| G by rewrite !gFnormal_trans. move=> minM sMG solM; have[/andP[ntM nMG] minM'] := mingroupP minM. apply/setIidPl/minM'; last exact: subsetIl. apply/andP; split; last by rewrite normsI // normal_norm. apply: meet_center_nil => //; first by apply: Fitting_nil. apply/andP; split; last exact: gFsub_trans. apply: Fitting_max; rewrite // /normal ?sMG //; apply: abelian_nil. by move: (minnormal_solvable_abelem minM solM) => /abelem_abelian. 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)