proposition: Lemma centrals_nil (s : seq {group gT}) G : G.-central.-series 1%G s -> last 1%G s = G -> nilpotent G.
proof: Proof. move=> cGs defG; apply/forall_inP=> H /subsetIP[sHG sHR]. move: sHG; rewrite -{}defG -subG1 -[1]/(gval 1%G). elim: s 1%G cGs => //= L s IHs K /andP[/and3P[sRK sKL sLG] /IHs sHL] sHs. exact: subset_trans sHR (subset_trans (commSg _ (sHL sHs)) sRK). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)