proposition: Lemma ucn1 G : 'Z_1(G) = 'Z(G).
proof: Proof. apply: (quotient_inj (normal1 _) (normal1 _)). by rewrite /= (ucn_central 0) -injmF ?norms1 ?coset1_injm. 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)