proposition: Lemma ucn_comm n G : [~: 'Z_n.+1(G), G] \subset 'Z_n(G).
proof: Proof. rewrite -quotient_cents2 ?normal_norm ?ucn_normal ?ucn_normalS //. by rewrite ucn_central subsetIr. 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)