proposition: Lemma nil_class_injm G : 'injm f -> G \subset D -> nil_class (f @* G) = nil_class G.
proof: Proof. move=> injf sGD; case nilG: (nilpotent G). apply/eqP; rewrite eqn_leq nil_class_morphim //. rewrite (sameP (lcn_nil_classP _ nilG) eqP) -subG1. rewrite -(injmSK injf) ?gFsub_trans // morphim1. by rewrite morphim_lcn // (lcn_nil_classP _ _ (leqnn _)) //= injm_nil. transitivity #|G|; apply/eqP; rewrite eqn_leq. rewrite -(card_injm injf sGD) (leq_trans (index_size _ _)) ?size_mkseq //. by rewrite leqNgt -nilpotent_class injm_nil ?nilG. rewrite (leq_trans (index_size _ _)) ?size_mkseq // leqNgt -nilpotent_class. by rewrite nilG. 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)