proposition: Lemma ucn_normalS n G : 'Z_n(G) <| 'Z_n.+1(G).
proof: Proof. by rewrite (normalS _ _ (ucn_normal n G)) ?ucn_subS ?ucn_sub. 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)