proposition: Lemma pradicalext_radicalext (E F : {subfield L}) : radical.-ext E F -> pradical.-ext E F.
proof: Proof. case=> [[/= n e pw]]; elim: n e pw E => [|n ih] e pw E Ee FE. by rewrite -FE tuple0 /= Fadjoin_nil; apply: rext_refl. apply: (@rext_trans _ << E; tnth e 0 >>). apply: (@pradicalext_radical (tnth pw 0)). by move/forallP/(_ ord0): Ee; rewrite take0 Fadjoin_nil. apply: (ih [tuple of behead e] [tuple of behead pw]) => /=; last first. by rewrite -adjoin_cons -drop1 (tnth_nth 0) -drop_nth 1?(drop0, size_tuple). apply/forallP=> /= i; move/forallP/(_ (rshift 1 i)): Ee => /=. rewrite !(tnth_nth 0, tnth_nth 0%N) !nth_behead [_ (rshift 1 i)]/=. by rewrite -adjoin_cons takeD drop1 (take_nth 0) 1?size_tuple // take0. 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)