proposition: Lemma ucnP G : reflect (exists n, 'Z_n(G) = G) (nilpotent G).
proof: Proof. apply: (iffP (lcnP G)) => -[n /eqP-clGn]; by exists n; apply/eqP; rewrite ucn_lcnP in clGn *. 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)