proposition: Lemma ucn_nilpotent n G : nilpotent 'Z_n(G).
proof: Proof. by apply/ucnP; exists n; rewrite ucn_id. 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)