proposition: Proposition coprime_cent_Fitting gT (A G : {group gT}) : A \subset 'N(G) -> coprime #|G| #|A| -> solvable G -> 'C_A('F(G)) \subset 'C(G).
proof: Proof. move=> nGA coGA solG; apply: subset_trans (subsetIr A _); set C := 'C_A(G). rewrite -quotient_sub1 /= -/C; last first. by rewrite subIset // normsI ?normG // norms_cent. apply: subset_trans (quotient_subcent _ _ _) _; rewrite /= -/C. have nCG: G \subset 'N(C) by rewrite cents_norm // centsC subsetIr. rewrite /= -(setIidPr (Fitting_sub _)) -[(G :&: _) / _](morphim_restrm nCG). rewrite injmF //=; last first. by rewrite ker_restrm ker_coset setIA (coprime_TIg coGA) subIset ?subxx. rewrite morphim_restrm -quotientE setIid. rewrite coprime_trivg_cent_Fitting ?quotient_norms ?coprime_morph //=. exact: morphim_sol. rewrite -strongest_coprime_quotient_cent ?trivg_quotient ?solG ?orbT //. by rewrite -setIA subsetIl. by rewrite coprime_sym -setIA (coprimegS (subsetIl _ _)). 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)