proposition: Lemma quotient_center_nil G : nilpotent (G / 'Z(G)) = nilpotent G.
proof: Proof. rewrite -ucn1; apply/idP/idP; last exact: quotient_nil. case/ucnP=> c nilGq; apply/ucnP; exists c.+1; have nsZ1G := ucn_normal 1 G. apply: (quotient_inj _ nsZ1G); last by rewrite /= -(addn1 c) quotient_ucn_add. by rewrite (normalS _ _ nsZ1G) ?ucn_sub ?ucn_sub_geq. 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)