proposition: Lemma morphim_ucn : GFunctor.pcontinuous (@upper_central_at n).
proof: Proof. by have [hZ ->] := ucn_pmap; apply: pmorphimF. 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)