proposition: Lemma ucnSnR n G : 'Z_n.+1(G) = [set x in G | [~: [set x], G] \subset 'Z_n(G)].
proof: Proof. apply/setP=> x; rewrite -(setIidPr (ucn_sub n.+1 G)) [LHS]inE [RHS]inE ucnSn. case Gx: (x \in G) => //=; have nZG := ucn_norm n G. rewrite -sub1set -sub_quotient_pre -?quotient_cents2 ?sub1set ?(subsetP nZG) //. by rewrite subsetI quotientS ?sub1set. 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)