proposition: Lemma pradicalext_radical n (x : L) (E : {subfield L}) : radical E x n -> pradical.-ext E << E; x >>%VS.
proof: Proof. move=> /radicalP[n_gt0 xnE]; have [k] := ubnP n. elim: k => // k IHk in n x E n_gt0 xnE *; rewrite ltnS => lenk. have [prime_n|primeN_n] := boolP (prime n). by apply: (@pradical_ext_Fadjoin n). case/boolP: (2 <= n)%N; last first. case: n {lenk primeN_n} => [|[]]// in xnE n_gt0 * => _. suff ->: <<E; x>>%VS = E by apply: rext_refl. by rewrite (Fadjoin_idP _). move: primeN_n => /primePn[|[d /andP[d_gt1 d_ltn] dvd_dn n_gt1]]. by case: ltngtP. have [m n_eq_md]: {k : nat | n = (k * d)%N}. by exists (n %/ d)%N; rewrite [LHS](divn_eq _ d) (eqP dvd_dn) addn0. have m_gt0 : (m > 0)%N. by move: n_gt0; rewrite !lt0n n_eq_md; apply: contra_neq => ->. apply: (@rext_trans _ <<E; x ^+ d>>) => //. apply: (@IHk m (x ^+ d)) => //. by rewrite -exprM mulnC -n_eq_md//. by rewrite (leq_trans _ lenk)// n_eq_md ltn_Pmulr. suff -> : <<E; x>>%AS = <<<<E; x ^+ d>>; x>>%AS. apply: (IHk d) => //. - by rewrite (leq_trans _ d_gt1)//. - by rewrite memv_adjoin. - by rewrite (leq_trans _ lenk). apply/val_inj; rewrite /= adjoinC [<<_; x ^+ d>>%VS](Fadjoin_idP _)//. by rewrite rpredX// memv_adjoin. 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)