proposition: Lemma radical_ext_solvable_ext (F0 : fieldType) (L : splittingFieldType F0) (E F : {subfield L}) : has_char0 L -> (E <= F)%VS -> solvable_by radical E F -> solvable_ext E F.
proof: Proof. move=> charL EF. move=> [_ /pradicalext_radicalext[[/= n e pw] /towerP epwP <- FK]]. have charF0 : [char F0] =i pred0 by move=> i; rewrite -charL char_lalg. pose k := n; suff {FK} : solvable_ext E <<E & take k e>>. by rewrite take_oversize ?size_tuple//; apply: sub_solvable_ext. elim: k => /= [|k IHsol]; first by rewrite take0 Fadjoin_nil. have [kn|nk] := ltnP k n; last first. by move: IHsol; rewrite !take_oversize ?size_tuple// leqW. rewrite (take_nth 0) ?size_tuple// adjoin_rcons. apply: solvable_ext_trans IHsol _. by rewrite /= subv_adjoin_seq subv_adjoin. have := epwP (Ordinal kn); rewrite (tnth_nth 0) (tnth_nth 0%N)/=. move=> /pradicalP[pwk_prime epwEk]. apply: (pradical_solvable_ext pwk_prime) => //. by have /charf0P-> := charF0; rewrite -lt0n prime_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)