proposition: Lemma nilpotent_sol G : nilpotent G -> solvable G.
proof: Proof. move=> nilG; apply/forall_inP=> H /subsetIP[sHG sHH']. by rewrite (forall_inP nilG) // subsetI sHG (subset_trans sHH') ?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)