proposition: Proposition stable_series_cent gT (A G : {group gT}) s : last 1%G s :=: G -> (A.-stable).-series 1%G s -> coprime #|G| #|A| -> solvable G -> A \subset 'C(G).
proof: Proof. move=> <-{G}; elim/last_ind: s => /= [|s G IHs]; first by rewrite cents1. rewrite last_rcons rcons_path /= => /andP[/IHs{IHs}]. move: {s}(last _ _) => H IH_H nHGA coGA solG; have [_ sHG _] := and3P nHGA. by rewrite (stable_factor_cent _ nHGA) ?IH_H ?(solvableS sHG) ?(coprimeSg sHG). 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)