proposition: Lemma solvableS G H : H \subset G -> solvable G -> solvable H.
proof: Proof. move=> sHG solG; apply/forall_inP=> K /subsetIP[sKH sKK']. by rewrite (forall_inP solG) // subsetI (subset_trans sKH). 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)