proposition: Lemma series_sol G H : H <| G -> solvable G = solvable H && solvable (G / H).
proof: Proof. case/andP=> sHG nHG; apply/idP/andP=> [solG | [solH solGH]]. by rewrite quotient_sol // (solvableS sHG). apply/forall_inP=> K /subsetIP[sKG sK'K]. suffices sKH: K \subset H by rewrite (forall_inP solH) // subsetI sKH. have nHK := subset_trans sKG nHG. rewrite -quotient_sub1 // subG1 (forall_inP solGH) //. by rewrite subsetI -morphimR ?morphimS. 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)