proposition: Lemma ucn_nil_classP n G : nilpotent G -> reflect ('Z_n(G) = G) (nil_class G <= n).
proof: Proof. move=> nilG; rewrite (sameP (lcn_nil_classP n nilG) eqP) ucn_lcnP; apply: eqP. 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)