proposition: Lemma morphim_nil G : nilpotent G -> nilpotent (f @* G).
proof: Proof. case/ucnP=> n ZnG; apply/ucnP; exists n; apply/eqP. by rewrite eqEsubset ucn_sub /= -{1}ZnG morphim_ucn. 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)