proposition: Lemma nilpotentS A B : B \subset A -> nilpotent A -> nilpotent B.
proof: Proof. move=> sBA nilA; apply/forall_inP=> H sHR. have:= forallP nilA H; rewrite (subset_trans sHR) //. by apply: subset_trans (setIS _ _) (setSI _ _); rewrite ?commgS. 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)