proposition: Lemma nil_class_morphim G : nilpotent G -> nil_class (f @* G) <= nil_class G.
proof: Proof. move=> nilG; rewrite (sameP (ucn_nil_classP _ (morphim_nil nilG)) eqP) /=. by rewrite eqEsubset ucn_sub -{1}(ucn_nil_classP _ nilG (leqnn _)) 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)