proposition: Lemma solvable_extP (E F : {subfield L}) : reflect (exists K : {subfield L}, [&& (F <= K)%VS, galois E K & solvable 'Gal(K / E)]) (solvable_ext E F).
proof: Proof. apply: (iffP idP) => [/andP[sepEF solEF]|[K /and3P[FK galEK solEK]]]. exists [aspace of normalClosure E F]. by rewrite normalClosure_galois ?normalClosureSr. have MsubK := galoisClosureP FK galEK; rewrite /solvable_ext. have sepEF : separable E F by case/and3P: galEK => [_ /separableSr->]. have /and3P [EsubM _ EnormM] := (normalClosure_galois sepEF). by rewrite -(isog_sol (normalField_isog galEK _ _)) ?EsubM ?quotient_sol ?andbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)