proposition: Lemma ucn_pmap : exists hZ : GFunctor.pmap, @upper_central_at n = hZ.
proof: Proof. elim: n => [|n' [hZ defZ]]; first by exists trivGfun_pgFun. by exists [pgFun of @center %% hZ]; rewrite /= -defZ. 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)