diff --git a/.nix/coq-overlays/mathcomp-abel/default.nix b/.nix/coq-overlays/mathcomp-abel/default.nix
new file mode 100644
index 0000000..3e30d6e
--- /dev/null
+++ b/.nix/coq-overlays/mathcomp-abel/default.nix
@@ -0,0 +1,27 @@
+{ coq, mkCoqDerivation, mathcomp, mathcomp-real-closed, lib, version ? null }:
+
+mkCoqDerivation {
+
+  namePrefix = [ "coq" "mathcomp" ];
+  pname = "abel";
+  owner = "math-comp";
+
+  inherit version;
+  defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ]  [
+      { cases = [ (range "8.10" "8.15") (isGe "1.12.0") ];           out = "1.2.0"; }
+      { cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; }
+    ] null;
+
+  release."1.2.0".sha256 = "1picd4m85ipj22j3b84cv8ab3330radzrhd6kp0gpxq14dhv02c2";
+  release."1.1.2".sha256 = "0565w713z1cwxvvdlqws2z5lgdys8lddf0vpwfdj7bpd7pq9hwxg";
+  release."1.0.0".sha256 = "190jd8hb8anqsvr9ysr514pm5sh8qhw4030ddykvwxx9d9q6rbp3";
+
+
+  propagatedBuildInputs = [ mathcomp.character mathcomp-real-closed ];
+
+  meta = with lib; {
+    description = "Abel - Galois and Abel - Ruffini Theorems";
+    license = licenses.cecill-b;
+    maintainers = [ maintainers.cohencyril ];
+  };
+}
diff --git a/_CoqProject b/_CoqProject
index 7f764d8..0289931 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,6 +6,7 @@ theories/xmathcomp/map_gal.v
 theories/xmathcomp/char0.v
 theories/xmathcomp/cyclotomic_ext.v
 theories/xmathcomp/real_closed_ext.v
+theories/xmathcomp/artin_scheier.v
 
 -R theories Abel
 -arg -w -arg -projection-no-head-constant
@@ -15,4 +16,4 @@ theories/xmathcomp/real_closed_ext.v
 -arg -w -arg -ambiguous-paths
 -arg -w -arg +non-primitive-record
 -arg -w -arg +undeclared-scope
--arg -w -arg +implicit-core-hint-db
\ No newline at end of file
+-arg -w -arg +implicit-core-hint-db
diff --git a/theories/abel.v b/theories/abel.v
index b7525f7..4180d11 100644
--- a/theories/abel.v
+++ b/theories/abel.v
@@ -1,7 +1,7 @@
 From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
 From mathcomp Require Import all_solvable all_field polyrcf.
 From Abel Require Import various classic_ext map_gal algR.
-From Abel Require Import char0 cyclotomic_ext real_closed_ext.
+From Abel Require Import char0 cyclotomic_ext real_closed_ext artin_scheier.
 
 (*****************************************************************************)
 (* We work inside a enclosing splittingFieldType L over a base field F0      *)
@@ -55,22 +55,31 @@ Proof. by case: splitP=> j eq_j; constructor; apply/val_inj. Qed.
 Section RadicalExtension.
 
 Variables (F0 : fieldType) (L : splittingFieldType F0).
-Hypothesis (charL : has_char0 L).
 
 Section Defs.
 
 Implicit Types (U V : {vspace L}).
 
-Definition radical U x n  := [&& (n > 0)%N & x ^+ n \in U].
-Definition pradical U x p := [&& prime p & x ^+ p \in U].
+Definition radical U x n := [||
+  [&& n%:R != 0 :> F0 & x ^+ n \in U] |
+  [&& n \in [char L] & x ^+ n - x \in U]].
+Definition pradical U x p := [||
+  [&& prime p, p%:R != 0 :> F0 & x ^+ p \in U] |
+  [&& p \in [char L] & x ^+ p - x \in U]].
 
-Lemma radicalP U x n : reflect  [/\ (n > 0)%N & x ^+ n \in U]
-                                [&& (n > 0)%N & x ^+ n \in U].
-Proof. exact/andP. Qed.
+Lemma radicalP U x n : reflect  [\/
+  [/\ n%:R != 0 :> F0 & x ^+ n \in U] |
+  [/\ n \in [char L] & x ^+ n - x \in U]]
+                                (radical U x n).
+Proof. by apply: (iffP orP); (case=> /andP h; [ left | right ]). Qed.
 
-Lemma pradicalP U x p : reflect [/\ prime p & x ^+ p \in U]
-                                [&& prime p & x ^+ p \in U].
-Proof. exact/andP. Qed.
+Lemma pradicalP U x p : reflect  [\/
+  [/\ prime p, p%:R != 0 :> F0 & x ^+ p \in U] |
+  [/\ p \in [char L] & x ^+ p - x \in U]]
+                                (pradical U x p).
+Proof.
+by apply: (iffP orP); (case=> h; [ left; apply/and3P | right; apply/andP ]).
+Qed.
 
 Implicit Types r : {vspace L} -> L -> nat -> bool.
 
@@ -149,46 +158,69 @@ Lemma solvable_by_radicals_radicalext (E F : {subfield L}) :
   radical.-ext E F -> solvable_by radical E F.
 Proof. by move=> extEF; exists F. Qed.
 
-Lemma radical_Fadjoin (n : nat) (x : L) (E : {subfield L}) :
-  (0 < n)%N -> x ^+ n \in E -> radical E x n.
-Proof. by move=> ? ?; apply/radicalP. Qed.
+Lemma radical_Fadjoin1 (n : nat) (x : L) (E : {subfield L}) :
+  n%:R != 0 :> F0 -> x ^+ n \in E -> radical E x n.
+Proof. by move=> ? ?; apply/radicalP; left. Qed.
+
+Lemma radical_Fadjoin2 (n : nat) (x : L) (E : {subfield L}) :
+  n \in [char L] -> x ^+ n - x \in E -> radical E x n.
+Proof. by move=> ? ?; apply/radicalP; right. Qed.
+
+Lemma pradical_Fadjoin1 (n : nat) (x : L) (E : {subfield L}) :
+  prime n -> n%:R != 0 :> F0 -> x ^+ n \in E -> pradical E x n.
+Proof. by move=> ? ? ?; apply/pradicalP; left. Qed.
+
+Lemma pradical_Fadjoin2 (n : nat) (x : L) (E : {subfield L}) :
+  n \in [char L] -> x ^+ n - x \in E -> pradical E x n.
+Proof. by move=> ? ?; apply/pradicalP; right. Qed.
 
-Lemma pradical_Fadjoin (n : nat) (x : L) (E : {subfield L}) :
-  prime n -> x ^+ n \in E -> pradical E x n.
-Proof. by move=> ? ?; apply/pradicalP. Qed.
+Lemma radical_ext_Fadjoin1 (n : nat) (x : L) (E : {subfield L}) :
+  n%:R != 0 :> F0 -> x ^+ n \in E -> radical.-ext E <<E; x>>%VS.
+Proof.  move=> n_gt0 xnE; apply/rext_r/(radical_Fadjoin1 n_gt0 xnE). Qed.
 
-Lemma radical_ext_Fadjoin (n : nat) (x : L) (E : {subfield L}) :
-  (0 < n)%N -> x ^+ n \in E -> radical.-ext E <<E; x>>%VS.
-Proof. by move=> n_gt0 xnE; apply/rext_r/(radical_Fadjoin n_gt0 xnE). Qed.
+Lemma radical_ext_Fadjoin2 (n : nat) (x : L) (E : {subfield L}) :
+  n \in [char L] -> x ^+ n - x \in E-> radical.-ext E <<E; x>>%VS.
+Proof. by move=> nL xnE; apply/rext_r/(radical_Fadjoin2 nL xnE). Qed.
 
-Lemma pradical_ext_Fadjoin (p : nat) (x : L) (E : {subfield L}) :
-  prime p -> x ^+ p \in E -> pradical.-ext E <<E; x>>%AS.
-Proof. by move=> p_prime Exn; apply/rext_r/(pradical_Fadjoin p_prime Exn). Qed.
+Lemma pradical_ext_Fadjoin1 (n : nat) (x : L) (E : {subfield L}) :
+  prime n -> n%:R != 0 :> F0 -> x ^+ n \in E -> pradical.-ext E <<E; x>>%VS.
+Proof.
+by move=> n_prime n0 xnE; apply/rext_r/(pradical_Fadjoin1 n_prime n0 xnE).
+Qed.
+
+Lemma pradical_ext_Fadjoin2 (n : nat) (x : L) (E : {subfield L}) :
+  n \in [char L] -> x ^+ n - x \in E-> pradical.-ext E <<E; x>>%VS.
+Proof. by move=> nL xnE; apply/rext_r/(pradical_Fadjoin2 nL xnE). Qed.
 
 Lemma pradicalext_radical n (x : L) (E : {subfield L}) :
   radical E x n -> pradical.-ext E << E; x >>%VS.
 Proof.
-move=> /radicalP[n_gt0 xnE]; have [k] := ubnP n.
+move=> /radicalP; case=> [[n_gt0] | [nL]] xnE; last first.
+  by apply: (pradical_ext_Fadjoin2 nL 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).
+  by apply: (@pradical_ext_Fadjoin1 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 move: n_gt0; rewrite eqxx.
+  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 => ->.
+have m_gt0 : m%:R != 0 :> F0.
+  by move: n_gt0; rewrite n_eq_md natrM; apply: contra_neq => ->; rewrite mul0r.
 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.
+  rewrite (leq_trans _ lenk)// n_eq_md ltn_Pmulr// lt0n.
+  by move: m_gt0; apply: contra_neq => ->.
 suff -> : <<E; x>>%AS = <<<<E; x ^+ d>>; x>>%AS.
   apply: (IHk d) => //.
-  - by rewrite (leq_trans _ d_gt1)//.
+  - by move: n_gt0; rewrite n_eq_md natrM; apply: contra_neq => ->;
+      rewrite mulr0.
   - by rewrite memv_adjoin.
   - by rewrite (leq_trans _ lenk).
 apply/val_inj; rewrite /= adjoinC [<<_; x ^+ d>>%VS](Fadjoin_idP _)//.
@@ -198,12 +230,13 @@ Qed.
 Lemma tower_sub r1 r2 n E (e : n.-tuple L) (pw : n.-tuple nat) :
   (forall U x n, r1 U x n -> r2 U x n) ->
     r1.-tower E e pw -> r2.-tower E e pw.
-Proof. by move=> sub_r /forallP /= h; apply/forallP=> /= i; apply/sub_r/h. Qed.
+Proof. by move=> sub_r /forallP /= h; apply/forallP => /= i; apply/sub_r/h. Qed.
 
 Lemma radical_pradical U x p : pradical U x p -> radical U x p.
 Proof.
-case/pradicalP=> prime_p xpU; apply/radicalP; split=> //.
-by case/primeP: prime_p => /ltnW.
+move=> /pradicalP x_rad; apply/radicalP.
+case: x_rad => x_rad; last by right.
+by case: x_rad => prime_p xpU; left; split.
 Qed.
 
 Lemma radicalext_pradicalext (E F : {subfield L}) :
@@ -223,7 +256,7 @@ apply: (@rext_trans _ << E; tnth e 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 => /=.
+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.
@@ -239,8 +272,10 @@ Proof. by case=> [R /pradicalext_radicalext ERe FR]; exists R. Qed.
 Lemma radicalext_Fadjoin_cyclotomic (E : {subfield L}) (w : L) (n : nat) :
   n.-primitive_root w -> radical.-ext E <<E; w>>%AS.
 Proof.
-move=> wprim; apply: (@radical_ext_Fadjoin n w E).
-  exact: prim_order_gt0 wprim.
+move=> wprim; apply: (@radical_ext_Fadjoin1 n w E).
+  apply/negP => /eqP n0.
+  move: (prim_root_natf_neq0 wprim).
+  by rewrite -scaler_nat n0 scale0r eqxx.
 by rewrite (prim_expr_order wprim) mem1v.
 Qed.
 
@@ -255,6 +290,7 @@ Local Notation "r .-tower" := (tower r)
   (at level 2, format "r .-tower") : ring_scope.
 Local Notation "r .-ext" := (extension_of r)
   (at level 2, format "r .-ext") : ring_scope.
+#[global] Hint Resolve rext_refl : core.
 
 (* Following the french wikipedia proof :
 https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_d%27Abel_(alg%C3%A8bre)#D%C3%A9monstration_du_th%C3%A9or%C3%A8me_de_Galois
@@ -279,61 +315,129 @@ Section Abel.
 (*                                                                            *)
 (******************************************************************************)
 
+Lemma radical_aimg (F0 : fieldType) (L L' : splittingFieldType F0)
+  (iota : 'AHom(L, L')) (U : {vspace L})
+  (x : Falgebra.vect_ringType L) (n : nat) :
+  radical (iota @: U) (iota x) n = radical U x n.
+Proof.
+rewrite /radical (fmorph_char (ahom_rmorphism iota))/=-rmorphX/= -rmorphB/=.
+have inE: forall y, iota y \in (iota @: U)%VS = (y \in U).
+  move=> y; apply/idP/idP.
+    by move=> /memv_imgP [u uU] /fmorph_inj ->.
+  by move=> /(memv_img iota).
+by rewrite 2!inE.
+Qed.
+
+Lemma radical_tower_aimg  (F0 : fieldType) (L L' : splittingFieldType F0)
+  (iota : 'AHom(L, L')) (E : {subfield L}) (e : ext_data L) :
+  radical.-tower (ext_size e) (iota @: E)
+  [tuple of [seq iota x | x <- ext_ep e]] (ext_pw e) =
+  radical.-tower (ext_size e) E (ext_ep e) (ext_pw e).
+Proof.
+apply/forallP/forallP => tower i /=.
+  move: (tower i).
+  by rewrite -map_take -aimg_adjoin_seq tnth_map radical_aimg.
+by rewrite -map_take -aimg_adjoin_seq tnth_map radical_aimg.
+Qed.
+
+Lemma radical_ext_aimg (F0 : fieldType) (L L' : splittingFieldType F0)
+  (iota : 'AHom(L, L')) (E F : {subfield L}):
+  radical.-ext (iota @: E) (iota @: F) <-> radical.-ext E F.
+Proof.
+split => [[]|[]] e tower img; last first.
+  exists (ExtData [tuple of [seq iota x | x <- ext_ep e]] (ext_pw e))=> /=.
+    by rewrite radical_tower_aimg.
+  by rewrite -aimg_adjoin_seq img.
+have /subset_limgP [f fF ef]: {subset (ext_ep e) <= (iota @: F)%VS}.
+  rewrite -img; exact: seqv_sub_adjoin.
+have sizef: size f == ext_size e by rewrite -(size_map iota) -ef size_tuple.
+set e' := ExtData (Tuple sizef) (ext_pw e).
+exists e'.
+  rewrite -(radical_tower_aimg iota)/=.
+  suff <-: ext_ep e = [tuple of [seq iota x | x <- ext_ep e']] by [].
+  by apply: val_inj.
+apply/eqP; rewrite -(@eq_limg_ker0 _ _ _ iota) ?AHom_lker0// aimg_adjoin_seq/=.
+by rewrite -ef img.
+Qed.
+
 Section Part1.
 Variables (F0 : fieldType) (L : splittingFieldType F0).
 Implicit Types (E F K : {subfield L}) (w : L) (n : nat).
 
-Lemma cyclic_radical_ext w E F (n := \dim_E F) :
-    n.-primitive_root w -> w \in E -> galois E F ->
-  cyclic 'Gal(F / E) -> radical.-ext E F.
-Proof.
-set G := (X in cyclic X) => w_root wE galois_EF /cyclicP[g GE].
-have EF := galois_subW galois_EF.
-have n_gt0 : (n > 0)%N by rewrite /n -dim_aspaceOver ?adim_gt0.
-have Gg : generator G g by rewrite GE generator_cycle.
-have gG : g \in G by rewrite GE cycle_id.
-have HT90g := Hilbert's_theorem_90 Gg (subvP EF _ wE).
-have /eqP/HT90g[x [xF xN0]] : galNorm E F w = 1.
-  rewrite /galNorm; under eq_bigr => g' g'G. rewrite (fixed_gal EF g'G)//. over.
-  by rewrite prodr_const -galois_dim// (prim_expr_order w_root).
+Lemma cyclic_radical_ext w E F : ((\dim_E F)`_[char L]^').-primitive_root w ->
+  w \in E -> galois E F -> cyclic 'Gal(F / E) -> radical.-ext E F.
+Proof.
+have [->//|NEF] := eqVneq (E : {vspace _}) F.
+have [n] := ubnP (\dim_E F); elim: n => // n IHn in w E F NEF *.
+rewrite ltnS leq_eqVlt => /predU1P[/[dup] dimEF ->|]; last exact: IHn.
+move=> wroot wE galEF /[dup] cycEF /cyclicP[/= g GE].
+have ggen : generator ('Gal(F / E))%g g by rewrite GE generator_cycle.
+have ggal : g \in ('Gal(F / E))%g by rewrite GE cycle_id.
+have EF := galois_subW galEF.
+have n_gt1 : (n > 1)%N.
+  rewrite -dimEF ltn_divRL ?field_dimS// mul1n.
+  by rewrite eqEdim EF/= -ltnNge in NEF.
+have n_gt0: (0 < n)%N by apply: leq_trans n_gt1.
+suff [k [a [k0 aE aF /rext_r arad]]]:
+  exists (k : nat) (a : L), [/\ (0 < k)%N, a \notin E, a \in F & radical E a k].
+  have gala: galois <<E; a>> F.
+    refine (galoisS _ galEF); apply/andP; split; first by apply: subv_adjoin.
+    by apply/FadjoinP; split=> //; apply/galois_subW.
+  have dimEaF: (\dim_(<<E; a>>) F < n)%N.
+    rewrite dim_Fadjoin mulnC divnMA dimEF ltn_Pdiv//.
+    by rewrite ltn_neqAle eq_sym adjoin_deg_eq1 aE//.
+  apply: rext_trans arad _; have [->//|Fne] := eqVneq <<E; a>>%AS F.
+  apply: (IHn (w ^+ (n`_[char L]^' %/ (\dim_(<<E; a>>) F)`_[char L]^')%N)) => //.
+  - rewrite dvdn_prim_root// partn_dvd//; apply/dvdnP; exists (\dim_E <<E; a>>).
+    by rewrite muln_dimv// ?subv_adjoin// galois_subW.
+  - by apply/rpredX/subvP_adjoin.
+  - exact (cyclicS (galS F (subv_adjoin E a)) cycEF).
+have [n0 | n_ne0] := boolP (n%:R == 0 :> L).
+  have [p pchar] := natf0_char n_gt0 n0; exists p.
+  have p_gt0 : (p > 0)%N by move: pchar => /andP [/prime_gt0].
+  have [|a aF] := Hilbert's_theorem_90_additive galEF ggen (rpredN1 _) _.
+    rewrite /galTrace; under eq_bigr do rewrite (fixed_gal EF) ?rpredN1//.
+    by rewrite sumr_const -galois_dim// dimEF -mulr_natl (eqP n0) mul0r.
+  have [aE|aNE] := boolP (a \in E).
+     by rewrite (fixed_gal EF)// subrr => /eqP; rewrite oppr_eq0 oner_eq0.
+  move=> /(canLR (addrNK _))/(canRL (addNKr _)) ga.
+  suff apE : a ^+ p - a \in E.
+    by exists a; split => //; apply/orP; right; apply/andP.
+  rewrite -(galois_fixedField galEF).
+  have apF : a ^+ p - a \in F by rewrite rpredB// rpredX.
+  apply/fixedFieldP => // h /[!GE]/cycleP[+ ->].
+  elim=> [|m IHm]; first by rewrite expg0 gal_id.
+  rewrite expgSr galM// IHm rmorphB/= rmorphX/= ga -Frobenius_autE.
+  by rewrite rmorphD/= rmorph1 !Frobenius_autE opprD addrACA subrr add0r.
+exists n; rewrite part_pnat_id -?natf_neq0// in wroot.
+have [|x [xF xN0]] := Hilbert's_theorem_90 ggen (subvP EF _ wE) _.
+  rewrite /galNorm; under eq_bigr do rewrite (fixed_gal EF)//.
+  by rewrite prodr_const -galois_dim// dimEF (prim_expr_order wroot).
 have gxN0 : g x != 0 by rewrite fmorph_eq0.
-have wN0 : w != 0 by rewrite (primitive_root_eq0 w_root) -lt0n.
+have wN0 : w != 0 by rewrite (primitive_root_eq0 wroot) -lt0n.
+have [xE|xNE] := boolP (x \in E).
+  rewrite (fixed_gal EF)// divff// => w1.
+  by rewrite w1 prim_root1// gtn_eqF in wroot.
 move=> /(canLR (mulfVK gxN0))/(canRL (mulKf wN0)) gx.
-have gXx i : (g ^+ i)%g x = w ^- i * x.
-  elim: i =>  [|i IHi].
-    by rewrite expg0 expr0 invr1 mul1r gal_id.
-  rewrite expgSr exprSr invfM galM// IHi rmorphM/= gx mulrA.
-  by rewrite (fixed_gal EF gG) ?rpredV ?rpredX.
-have ExF : (<<E; x>> <= F)%VS by exact/FadjoinP.
-suff -> : F = <<E; x>>%AS.
-  apply: radical_ext_Fadjoin n_gt0 _.
-  rewrite -(galois_fixedField galois_EF) -/G GE.
-  apply/fixedFieldP; first by rewrite rpredX.
-  move=> _ /cycleP[i ->]; rewrite rmorphX/= gXx exprMn exprVn exprAC.
-  by rewrite (prim_expr_order w_root)// expr1n invr1 mul1r.
-apply/val_inj/eqP => /=.
-have -> : F = fixedField (1%g : {set gal_of F}) :> {vspace L}.
-  by apply/esym/eqP; rewrite -galois_eq ?galvv ?galois_refl//.
-rewrite -galois_eq; last by apply: galoisS galois_EF; rewrite subv_adjoin.
-rewrite -subG1; apply/subsetP => g' g'G'.
-have /cycleP[i g'E]: g' \in <[g]>%g.
-  rewrite -GE gal_kHom//; apply/kAHomP => y yE.
-  by rewrite (fixed_gal _ g'G') ?subvP_adjoin.
-rewrite g'E in g'G' *.
-have : (g ^+ i)%g x = x by rewrite (fixed_gal _ g'G') ?memv_adjoin.
-rewrite gXx => /(canRL (mulfK xN0))/eqP; rewrite divff// invr_eq1.
-rewrite -(prim_order_dvd w_root) => dvdni.
-have /exponentP->// : (exponent G %| i)%N.
-by rewrite GE exponent_cycle orderE -GE -galois_dim.
+have nF0_ne0: n%:R != 0 :> F0.
+  by rewrite natf0_partn// -(eq_partn _ (@char_lalg _ L)) -natf0_partn.
+suff: x ^+ n \in E by exists x; split => //; apply/orP; left; apply/andP.
+rewrite -(galois_fixedField galEF).
+have xnF : x ^+ n \in F by rewrite rpredX.
+apply/fixedFieldP => //= h /[!GE]/cycleP[+ ->].
+elim=> [|m IHm]; first by rewrite expg0 gal_id.
+rewrite expgSr galM// IHm rmorphX/= gx exprMn exprVn.
+by rewrite (prim_expr_order wroot) invr1 mul1r.
 Qed.
 
 Lemma solvableWradical_ext w E F (n := \dim_E F) :
-    n.-primitive_root w -> w \in E -> galois E F ->
+  (n`_[char L]^').-primitive_root w -> w \in E -> galois E F ->
   solvable 'Gal(F / E) -> radical.-ext E F.
 Proof.
 move=> + + galEF; have [k] := ubnP n; elim: k => // k IHk in w E F n galEF *.
 rewrite ltnS => le_nk; have subEF : (E <= F)%VS by case/andP: galEF.
-have n_gt0 : (0 < n)%N by rewrite ltn_divRL ?field_dimS// mul0n adim_gt0.
+move=> /[dup]/prim_root_natf_neq0 n_ne0.
+have n_gt0: (0 < n)%N by rewrite divn_gt0 ?adim_gt0//; apply/dimvS.
 move=> wn Ew solEF; have [n_le1|n_gt1] := leqP n 1%N.
   have /eqP : n = 1%N by case: {+}n n_gt0 n_le1 => [|[]].
   rewrite -eqn_mul ?adim_gt0 ?field_dimS// mul1n eq_sym dimv_leqif_eq//.
@@ -348,38 +452,45 @@ pose d := \dim_E (fixedField H); pose p := \dim_(fixedField H) F.
 have p_gt0 : (p > 0)%N by rewrite divn_gt0 ?adim_gt0 ?dimvS ?fixedField_bound.
 have n_eq : n = (p * d)%N by rewrite /p /d -dim_fixedField dim_fixed_galois;
                              rewrite ?Lagrange ?normal_sub -?galois_dim.
-have Ewm : w ^+ (n %/ d) \in E by rewrite rpredX.
+have Ewm : w ^+ (n`_[char L]^' %/ d`_[char L]^')%N \in E by rewrite rpredX.
 move=> /prime_cyclic/cyclic_radical_ext-/(_ _ _ Ewm galEH)/=.
-rewrite dvdn_prim_root// => [/(_ isT)|]; last by rewrite n_eq dvdn_mull.
-move=> /rext_trans; apply; apply: (IHk (w ^+ (n %/ p))) => /=.
+rewrite -/d dvdn_prim_root// => [/(_ isT)|];
+  last by rewrite partn_dvd// n_eq dvdn_mull.
+move=> /rext_trans; apply.
+apply: (IHk (w ^+ (n`_[char L]^' %/ p`_[char L]^'))) => /=.
 - exact: fixedField_galois.
 - rewrite (leq_trans _ le_nk)// -dim_fixedField /n galois_dim// proper_card//.
   by rewrite properEneq H_neq normal_sub.
-- by rewrite dvdn_prim_root// n_eq dvdn_mulr.
+- by rewrite -/p dvdn_prim_root// partn_dvd// n_eq dvdn_mulr.
 - by rewrite rpredX//; apply: subvP Ew.
 - by rewrite gal_fixedField (solvableS (normal_sub Hnormal)).
 Qed.
 
 Lemma galois_solvable_by_radical w E F (n := \dim_E F) :
-    n.-primitive_root w -> galois E F ->
+    (n`_[char L]^')%N.-primitive_root w -> galois E F ->
   solvable 'Gal(F / E) -> solvable_by radical E F.
 Proof.
 move=> w_root galEF solEF; have [EF Ew] := (galois_subW galEF, subv_adjoin E w).
 exists (F * <<E; w>>)%AS; last by rewrite field_subvMr.
 apply: rext_trans (radicalext_Fadjoin_cyclotomic _ w_root) _.
 have galEwFEw: galois <<E; w>> (F * <<E; w>>) by apply: galois_prodvr galEF.
-pose m := \dim_<<E; w>> (F * <<E; w>>); pose w' := w ^+ (n %/ m).
+pose m := \dim_<<E; w>> (F * <<E; w>>).
+pose w' := w ^+ (n`_[char L]^' %/ m`_[char L]^')%N.
 have w'Ew : w' \in <<E; w>>%VS by rewrite rpredX ?memv_adjoin.
-have w'prim : m.-primitive_root w'.
+have w'prim : (m`_[char L]^')%N.-primitive_root w'.
   rewrite dvdn_prim_root // /m /n !galois_dim//.
-  by rewrite (card_isog (galois_isog galEF _)) ?cardSg ?galS ?subv_cap ?EF//.
-apply: (@solvableWradical_ext w'); rewrite // (isog_sol (galois_isog galEF _))//.
+  rewrite (card_isog (galois_isog galEF _))// partn_dvd//.
+  by rewrite cardSg ?galS ?subv_cap ?EF//.
+apply: (@solvableWradical_ext w') => //.
+rewrite (isog_sol (galois_isog galEF _))//.
 by rewrite (solvableS _ solEF) ?galS// subv_cap EF.
 Qed.
 
 (* Main lemma of part 1 *)
 Lemma ext_solvable_by_radical w E F (n := \dim_E (normalClosure E F)) :
-  n.-primitive_root w -> solvable_ext E F -> solvable_by radical E F.
+  (n`_[char L]^')%N.-primitive_root w ->
+  solvable_ext E F ->
+  solvable_by radical E F.
 Proof.
 move=> wprim /andP[sepEF]; have galEF := normalClosure_galois sepEF.
 move=> /(galois_solvable_by_radical wprim galEF) [M EM EFM]; exists M => //.
@@ -547,13 +658,27 @@ rewrite (@pradical_solvable p _ _ w)// ?memv_adjoin//.
 by rewrite (isog_sol (normalField_isog _ _ _)) ?galois_normalW ?subv_adjoin.
 Qed.
 
+Lemma ArtinSchreier_solvable_ext (p : nat) (F0 : fieldType)
+    (L : splittingFieldType F0) (E : {subfield L}) (x : L) : p \in [char L] ->
+  x ^+ p - x \in E -> x \notin E -> solvable_ext E <<E; x>>.
+Proof.
+move=> pchar xpE xE.
+apply/solvable_extP; exists <<E; x>>%AS; rewrite subvv/=.
+rewrite (ArtinSchreier_galois pchar xpE)/=.
+apply/abelian_sol/cyclic_abelian/prime_cyclic.
+rewrite -(galois_dim (ArtinSchreier_galois pchar xpE)) -adjoin_degreeE.
+rewrite (pred_Sn (adjoin_degree E x)) -size_minPoly (minPoly_ArtinSchreier pchar)//.
+move: pchar => /andP[pprim _].
+rewrite -addrA -opprD size_addl size_polyXn// size_opp size_XaddC ltnS.
+by apply: prime_gt1.
+Qed.
+
 Lemma radical_ext_solvable_ext (F0 : fieldType) (L : splittingFieldType F0)
-    (E F : {subfield L}) : has_char0 L -> (E <= F)%VS ->
+    (E F : {subfield L}) : (E <= F)%VS ->
   solvable_by radical E F -> solvable_ext E F.
 Proof.
-move=> charL EF.
+move=> 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.
@@ -563,9 +688,11 @@ 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.
+move=> /pradicalP; case=> [[pwk_prime] | [pwkL]] epwEk.
+  by apply: (pradical_solvable_ext pwk_prime).
+case /boolP: (e`_k \in <<E & take k e>>%VS).
+  move=> /Fadjoin_idP ->; exact: solvable_ext_refl.
+by apply: (ArtinSchreier_solvable_ext pwkL).
 Qed.
 
 (******************************************************************************)
@@ -576,11 +703,11 @@ Qed.
 
 (** Ok **)
 Lemma AbelGalois  (F0 : fieldType) (L : splittingFieldType F0) (w : L)
-  (E F : {subfield L}) : (E <= F)%VS -> has_char0 L ->
-  (\dim_E (normalClosure E F)).-primitive_root w ->
+  (E F : {subfield L}) (n := \dim_E (normalClosure E F)) : (E <= F)%VS ->
+  (n`_[char L]^')%N.-primitive_root w ->
   solvable_by radical E F <-> solvable_ext E F.
 Proof.
-move=> EF charL wprim; split; first exact: radical_ext_solvable_ext.
+move=> EF wprim; split; first exact: radical_ext_solvable_ext.
 exact: (ext_solvable_by_radical wprim).
 Qed.
 
@@ -589,7 +716,7 @@ End Abel.
 Definition solvable_by_radical_poly (F : fieldType) (p : {poly F}) :=
   forall (L : splittingFieldType F) (rs : seq L),
     p ^^ in_alg L %= \prod_(x <- rs) ('X - x%:P) ->
-    forall w : L, (\dim <<1 & rs>>%VS).-primitive_root w ->
+    forall w : L, ((\dim <<1 & rs>>%VS)`_[char L]^')%N.-primitive_root w ->
     solvable_by radical 1 <<1 & rs>>.
 
 Definition solvable_ext_poly (F : fieldType) (p : {poly F}) :=
@@ -597,6 +724,10 @@ Definition solvable_ext_poly (F : fieldType) (p : {poly F}) :=
     p ^^ in_alg L %= \prod_(x <- rs) ('X - x%:P) ->
     solvable 'Gal(<<1 & rs>> / 1).
 
+Definition separable_splittingField (F : fieldType) (p : {poly F}) :=
+  forall (L : splittingFieldType F) (rs : seq L),
+    p ^^ in_alg L %= \prod_(x <- rs) ('X - x%:P) -> separable 1 <<1 & rs>>.
+
 Lemma galois_solvable (F0 : fieldType) (L : splittingFieldType F0)
       (E F : {subfield L}) :
   galois E F -> solvable_ext E F = solvable 'Gal(F / E).
@@ -605,50 +736,55 @@ by move=> /and3P[EF sEF nEF]; rewrite /solvable_ext sEF normalClosure_id.
 Qed.
 
 Lemma normal_solvable  (F0 : fieldType) (L : splittingFieldType F0)
-      (E F : {subfield L}) : has_char0 L ->
+      (E F : {subfield L}) : separable E F ->
   (E <= F)%VS -> normalField E F -> solvable_ext E F = solvable 'Gal(F / E).
-Proof. by move=> charL EF /(char0_galois charL EF)/galois_solvable. Qed.
+Proof.
+move=> /normalClosure_galois /[swap] EF /[swap] /(normalClosure_id EF) ->.
+by apply: galois_solvable.
+Qed.
 
-Lemma AbelGaloisPoly (F : fieldType) (p : {poly F}) : has_char0 F ->
+Lemma AbelGaloisPoly (F : fieldType) (p : {poly F}) :
+  separable_splittingField p ->
   solvable_ext_poly p <-> solvable_by_radical_poly p.
 Proof.
-move=> charF; split=> + L rs pE => [/(_ L rs pE) + w w_prim|solrs]/=.
-  have charL : has_char0 L by move=> i; rewrite char_lalg.
+move=> psep.
+split=> + L rs pE => [/(_ L rs pE) + w w_prim|solrs]/=.
   have normal_rs : normalField 1 <<1 & rs>>.
     apply/splitting_normalField; rewrite ?sub1v//.
     by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs].
-  by move=> solrs; apply/(@AbelGalois _ _ w);
-     rewrite ?char0_solvable_extE ?normalClosure_id ?sub1v ?dimv1 ?divn1.
-have charL : has_char0 L by move=> i; rewrite char_lalg.
-have seprs: separable 1 <<1 & rs>> by apply/char0_separable.
+  move=> solrs; apply/(@AbelGalois _ _ w);
+  rewrite ?normalClosure_id ?sub1v ?dimv1 ?divn1//.
+  by rewrite /solvable_ext normalClosure_id ?sub1v// solrs andbT psep.
 have normal_rs : normalField 1 <<1 & rs>>.
   apply/splitting_normalField; rewrite ?sub1v//.
   by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs].
 pose n := \dim <<1 & rs>>.
-have nFN0 : n%:R != 0 :> F by have /charf0P-> := charF; rewrite -lt0n adim_gt0.
-apply: (@classic_cycloSplitting _ L _ nFN0) => - [L' [w [iota wL' w_prim]]].
+apply: (@classic_cycloSplitting _ L _ (natf_partn_ne0 F n)).
+move=> - [L' [w [iota wL' w_prim]]].
 suff: solvable_ext 1 <<1 & rs>>.
-  by rewrite /solvable_ext seprs normalClosure_id ?sub1v.
+   by rewrite /solvable_ext psep// normalClosure_id ?sub1v.
 rewrite -(solvable_ext_aimg iota).
-have charL' : [char L'] =i pred0 by move=> i; rewrite char_lalg.
+have nE: ((\dim <<1 & rs>>%AS)`_[char L']^' = n`_[char F]^')%N.
+  apply/eq_partn/eq_negn => x.
+  by rewrite -(char_lalg L); apply/fmorph_char/ahom_rmorphism.
 apply/(@AbelGalois _ _ w) => //.
 - by rewrite limgS// sub1v.
 - rewrite -aimg_normalClosure //= aimg1 dimv1 divn1 dim_aimg/=.
-  by rewrite normalClosure_id ?dimv1 ?divn1 ?sub1v//.
+  by rewrite normalClosure_id ?sub1v// nE.
 have /= := solrs L' (map iota rs) _ w.
 rewrite -(aimg1 iota) -!aimg_adjoin_seq dim_aimg.
 apply => //; have := pE; rewrite -(eqp_map [rmorphism of iota]).
-by rewrite -map_poly_comp/= (eq_map_poly (rmorph_alg _)) map_prod_XsubC.
+   by rewrite -map_poly_comp/= (eq_map_poly (rmorph_alg _)) map_prod_XsubC.
+by rewrite nE.
 Qed.
 
 Lemma solvable_ext_polyP (F : fieldType) (p : {poly F}) : p != 0 ->
-    has_char0 F ->
   solvable_ext_poly p <->
   classically (exists (L : splittingFieldType F) (rs : seq L),
                 p ^^ in_alg L %= \prod_(x <- rs) ('X - x%:P) /\
                 solvable 'Gal(<<1 & rs>> / 1)).
 Proof.
-move=> p_neq0 charF; split => sol_p.
+move=> p_neq0; split => sol_p.
 have FoE (v : F^o) : v = in_alg F^o v by rewrite /= /(_%:A)/= mulr1.
 apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0).
   move=> [L [rs [iota rsf p_eq]]]; apply/classicW.
@@ -663,8 +799,6 @@ apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0).
   exists S, rs; split => //=; first by rewrite -(eq_map_poly iotaF).
   by apply: (sol_p S rs); rewrite -(eq_map_poly iotaF).
 move=> L rs prs; apply: sol_p => -[M [rs' [prs']]].
-have charL : has_char0 L by move=> n; rewrite char_lalg charF.
-have charM : has_char0 M by move=> n; rewrite char_lalg charF.
 pose K := [fieldExtType F of subvs_of <<1 & rs>>%VS].
 pose rsK := map (vsproj <<1 & rs>>%VS) rs.
 have pKrs : p ^^ in_alg K %= \prod_(x <- rsK) ('X - x%:P).
@@ -695,23 +829,23 @@ by rewrite -imgg -(aimg1 g)/= -img_map_gal injm_sol ?map_gal_inj ?subsetT//.
 Qed.
 
 Lemma solvable_by_radical_polyP (F : fieldType) (p : {poly F}) : p != 0 ->
-    has_char0 F ->
+  separable_splittingField p ->
   solvable_by_radical_poly p <->
   classically (exists (L : splittingFieldType F) (rs : seq L),
                 p ^^ in_alg L %= \prod_(x <- rs) ('X - x%:P) /\
                 solvable_by radical 1 <<1 & rs>>).
 Proof.
-move=> p_neq0 charF0;
+move=> p_neq0 psep;
 split => sol_p; last first.
   apply/AbelGaloisPoly => //; apply/solvable_ext_polyP => //.
   apply: classic_bind sol_p => -[L [rs [prs sol_p]]]; apply/classicW.
   exists L, rs; split => //; rewrite -galois_solvable.
     apply: radical_ext_solvable_ext; rewrite ?sub1v// => v.
-    by rewrite char_lalg charF0.
-  have charL : has_char0 L by move=> n; rewrite char_lalg charF0.
-  rewrite char0_galois// ?sub1v//.
-  apply/splitting_normalField; rewrite ?sub1v//.
-  by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs].
+  move: (psep L rs prs) => /normalClosure_galois; congr galois.
+  apply: normalClosure_id; first by rewrite sub1v.
+  apply/splitting_normalField; first by rewrite sub1v.
+  exists (p ^^ in_alg L); first by apply/polyOver1P; exists p.
+  by exists rs.
 have FoE (v : F^o) : v = in_alg F^o v by rewrite /= /(_%:A)/= mulr1.
 apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0).
 move=> [L [rs [f rsf p_eq]]].
@@ -722,15 +856,16 @@ have splitL : SplittingField.axiom L.
   apply/eqP; rewrite eqEsubv sub1v andbT; apply/subvP => v.
   by move=> /memv_imgP[u _ ->]; rewrite fF/= rpredZ// rpred1.
 pose S := SplittingFieldType F L splitL.
-pose d := \dim  <<1 & (rs : seq S)>>.
-have /classic_cycloSplitting-/(_ S) : d%:R != 0 :> F.
-  by have /charf0P-> := charF0; rewrite -lt0n adim_gt0.
+pose d := ((\dim <<1 & (rs : seq S)>>)`_[char F]^')%N.
+have /classic_cycloSplitting-/(_ S) : d%:R != 0 :> F by apply: natf_partn_ne0.
 apply/classic_bind => -[C [w [g wg w_prim]]]; apply/classicW.
 have gf : g \o f =1 in_alg C by move=> v /=; rewrite fF rmorph_alg.
 have pgrs : p ^^ in_alg C %= \prod_(x <- [seq g i | i <- rs]) ('X - x%:P).
   by rewrite -(eq_map_poly gf) map_poly_comp/= -map_prod_XsubC eqp_map//.
 exists C, (map g rs); split => //=; apply: (sol_p C (map g rs) _ w) => //.
-by rewrite -(aimg1 g) -aimg_adjoin_seq dim_aimg.
+rewrite -(aimg1 g) -aimg_adjoin_seq dim_aimg.
+move: w_prim; congr (_.-primitive_root w); apply/eq_partn/eq_negn => x.
+by rewrite -(char_lalg C).
 Qed.
 
 Import GRing.Theory Order.Theory Num.Theory.
@@ -774,7 +909,10 @@ have splitS : splittingFieldFor 1 (p ^^ in_alg S) fullv by exists rs.
 have splitS' : splittingFieldFor 1 (p ^^ in_alg S') <<1 & rs'>> by exists rs'.
 have [f /= imgf] := splitting_ahom splitS splitS'.
 exists S', iota', rs'; split => //.
-by apply: (p_sol S' rs' prs' w); rewrite -imgf dim_aimg/= -rsf.
+apply: (p_sol S' rs' prs' w); rewrite -imgf dim_aimg/= -rsf.
+move: w_prim; congr (_.-primitive_root w).
+rewrite -(partnC [char L'] d_gt0) (eq_partn _ (char_ext L')) -/d {1}/partn.
+by rewrite -big_filter filter_pred0 big_nil mul1n.
 Qed.
 
 Lemma splitting_num_field (p : {poly rat}) :
@@ -807,6 +945,7 @@ move=> p_neq0; split.
   by exists L, <<1 & rs>>%AS; first by exists rs.
 have charrat : [char rat] =i pred0 by exact: char_num.
 move=> [L [K [rs prs <-] solK]]; apply/solvable_by_radical_polyP => //.
+  by move=> L' rs' _; apply/char0_separable/char_ext.
 by apply/classicW; exists L, rs.
 Qed.
 
@@ -855,7 +994,8 @@ apply: (equivP idP); rewrite -AbelGaloisPoly//.
 have [rs prs <-] := numfieldP p_neq0.
 split; last by move=> /(_ (numfield p) rs prs).
 move=> solp; apply/solvable_ext_polyP => //.
-by apply/classicW; exists (numfield p); exists rs; split.
+  by apply/classicW; exists (numfield p); exists rs; split.
+by move=> L rs _; apply/char0_separable/char_ext.
 Qed.
 
 Definition numfield_roots (p : {poly rat}) :=
@@ -1504,7 +1644,8 @@ have Cchar := Cchar => p_neq0; split.
   - by move=> _ [f1 <-] _ [f2 <-]; exists (BinOp op f1 f2).
   have /Fadjoin_polyP[q qk ->] := subvsP s.
   have /towerP/(_ ord0) := epw; rewrite !tnth0/= Fadjoin_nil.
-  move=> /radicalP[]; case: i => // i in epw * => _ uik.
+  move=> /radicalP[][]; last by rewrite char_ext.
+  case: i => // i in epw * => _ uik.
   pose v := i.+1.-root (iota (u ^+ i.+1)).
   have : ('X ^+ i.+1 - (v ^+ i.+1)%:P).[iota u] == 0.
     by rewrite !hornerE ?hornerXn rootCK// rmorphX subrr.
@@ -1524,7 +1665,8 @@ have Cchar := Cchar => p_neq0; split.
   case: IHq => // fq fq_eq.
   exists (fq * fu + Base (Subvs ck))%algT => /=.
   by rewrite rmorphD rmorphM/= map_polyX map_polyC !hornerE fq_eq.
-move=> mkalg; apply/solvable_by_radical_polyP => //=; first exact: char_num.
+move=> mkalg; apply/solvable_by_radical_polyP => //=.
+  by move=> L rs _; apply/char0_separable/char_ext.
 have [/= rsalg pE] := closed_field_poly_normal (p ^^ (ratr : _ -> algC)).
 have {}pE : p ^^ ratr %= \prod_(z <- rsalg) ('X - z%:P).
   rewrite pE (eqp_trans (eqp_scale _ _)) ?eqpxx//.
@@ -1599,11 +1741,10 @@ elim: f => //= [x|c|u f1 IHf1|b f1 IHf1 f2 IHf2] in k {r fr} als1 als1E *.
   by rewrite [RHS](fmorph_eq_rat [rmorphism of iota \o in_alg _]).
 - case: als1 als1E => [|y []]//= []/=; rewrite adjoin_seq1.
   case: c => [/eqP|/eqP|n yomega].
-  + rewrite fmorph_eq0 => /eqP->; rewrite (Fadjoin_idP _) ?rpred0//.
-    exact: rext_refl.
-  + rewrite fmorph_eq1 => /eqP->; rewrite (Fadjoin_idP _) ?rpred1//.
-    exact: rext_refl.
-  + apply/(@rext_r _ _ _ n.+1)/radicalP; split => //.
+  + by rewrite fmorph_eq0 => /eqP->; rewrite (Fadjoin_idP _) ?rpred0.
+  + by rewrite fmorph_eq1 => /eqP->; rewrite (Fadjoin_idP _) ?rpred1.
+  + apply/(@rext_r _ _ _ n.+1)/radicalP; left; split.
+      by apply/negP; rewrite pnatr_eq0.
     rewrite prim_expr_order ?rpred1//.
     by rewrite -(fmorph_primitive_root iota) yomega prim1rootP.
 - case: als1 als1E => //= a l [IHl IHlu].
@@ -1619,7 +1760,8 @@ elim: f => //= [x|c|u f1 IHf1|b f1 IHf1 f2 IHf2] in k {r fr} als1 als1E *.
     by have /fmorph_inj-> := IHl; rewrite rpredV.
   + rewrite (Fadjoin_idP _); first exact: rext_refl.
     by have := IHl; rewrite -rmorphX => /fmorph_inj->; rewrite rpredX.
-  apply/(@rext_r _ _ _ n.+1)/radicalP; split => //.
+  apply/(@rext_r _ _ _ n.+1)/radicalP; left; split.
+    by apply/negP; rewrite pnatr_eq0.
   have /(congr1 ((@GRing.exp _)^~ n.+1)) := IHl.
   by rewrite rootCK// -rmorphX => /fmorph_inj->.
 - case: als1 als1E => //= a l [IHl IHlu].
diff --git a/theories/xmathcomp/artin_scheier.v b/theories/xmathcomp/artin_scheier.v
new file mode 100644
index 0000000..733faf0
--- /dev/null
+++ b/theories/xmathcomp/artin_scheier.v
@@ -0,0 +1,120 @@
+From mathcomp Require Import all_ssreflect all_fingroup all_algebra.
+From mathcomp Require Import all_solvable all_field polyrcf.
+From Abel Require Import various classic_ext map_gal algR.
+From Abel Require Import char0 cyclotomic_ext real_closed_ext.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import GRing.Theory.
+
+Local Open Scope ring_scope.
+
+Section ArtinSchreier.
+Variable (p : nat) (F0 : fieldType) (L : splittingFieldType F0).
+Variable (E : {subfield L}) (x : L).
+Hypothesis (pchar : p \in [char L]) (xpE : x ^+ p - x \in E).
+
+Let pprim : prime p.
+Proof. by move: pchar => /andP[]. Qed.
+
+Let p0 : p%:R == 0 :> L.
+Proof. by move: pchar => /andP[_]. Qed.
+
+Let p_gt0 : (0 < p)%N.
+Proof. by apply: prime_gt0. Qed.
+
+Let p1 : (1 < p)%N.
+Proof. by apply: prime_gt1. Qed.
+
+Let rs := [tuple x + i%:R | i < p].
+
+Let AS := 'X^p - 'X - (x ^+ p - x)%:P.
+
+Let x_rs : x \in rs.
+Proof.
+apply/tnthP; exists (Ordinal p_gt0).
+by rewrite tnth_map/= tnth_ord_tuple/= addr0.
+Qed.
+
+Lemma ArtinSchreier_factorize : AS = \prod_(i < p) ('X - (x + i%:R)%:P).
+Proof.
+have sNXXp : (size ('X : {poly L}) < size ('X^p : {poly L}))%N.
+  by rewrite size_polyXn size_polyX.
+have sCXp (c : L) : (size c%:P < size ('X^p : {poly L}))%N.
+  by rewrite size_polyXn ltnS (leq_trans (size_polyC_leq1 _)) ?prime_gt0.
+have lcLHS : lead_coef ('X^p - 'X - (x ^+ p - x)%:P) = 1.
+  by rewrite !lead_coefDl ?lead_coefXn ?scale1r// ?size_addl ?size_opp.
+rewrite [LHS](@all_roots_prod_XsubC _ _ rs).
+- by rewrite lcLHS scale1r big_map big_enum.
+- by rewrite size_tuple ?size_addl ?size_opp// size_polyXn.
+- apply/allP => y /mapP[/= i _ ->]; rewrite rootE !hornerE hornerXn.
+  rewrite -!Frobenius_autE rmorphD rmorph_nat.
+  by rewrite opprD addrACA subrr addr0 subrr.
+- by rewrite uniq_rootsE/= map_inj_uniq ?enum_uniq// => i j /addrI/ZprI; apply.
+Qed.
+
+Let ASE : AS = \prod_(i <- rs) ('X - i%:P).
+Proof. by rewrite ArtinSchreier_factorize big_image/=. Qed.
+
+Lemma ArtinSchreier_splitting : splittingFieldFor E AS <<E; x>>%AS.
+Proof.
+exists rs; first by rewrite ASE eqpxx.
+have /eq_adjoin-> : rs =i x :: rem x rs by apply/perm_mem/perm_to_rem.
+rewrite adjoin_cons (Fadjoin_seq_idP _)//=.
+apply/allP => y /mem_rem /mapP[i _ ->]/=.
+by rewrite rpredD ?memv_adjoin// subvP_adjoin// rpredMn// rpred1.
+Qed.
+
+Lemma ArtinSchreier_polyOver : AS \is a polyOver E.
+Proof. by rewrite rpredB ?polyOverC// rpredB ?rpredX// polyOverX. Qed.
+
+Lemma ArtinSchreier_galois : galois E <<E; x>>.
+Proof.
+apply/splitting_galoisField; exists ('X^p - 'X - (x ^+ p - x)%:P); split.
+- exact ArtinSchreier_polyOver.
+- rewrite /separable_poly derivB derivC subr0 derivB derivXn derivX -scaler_nat.
+  rewrite charf0// scale0r add0r -(@coprimepZr _ (-1)) ?oppr_eq0 ?oner_eq0//.
+  by rewrite scaleNr scale1r opprK coprimep1.
+- by apply: ArtinSchreier_splitting.
+Qed.
+
+Lemma minPoly_ArtinSchreier : x \notin E -> minPoly E x = AS.
+Proof.
+move=> xE; have /(minPoly_dvdp ArtinSchreier_polyOver) : root AS x.
+  by rewrite ASE root_prod_XsubC.
+rewrite ASE => /dvdp_prod_XsubC[m]; rewrite eqp_monic ?monic_minPoly//;
+  last by rewrite monic_prod// => i _; rewrite monic_XsubC.
+rewrite -map_mask.
+have [{}m sm ->] := resize_mask m (enum 'I_p).
+set s := mask _ _ => /eqP mEx.
+have [|smp_gt0] := posnP (size s).
+  case: s mEx => // /(congr1 (horner^~x))/esym/eqP.
+  by rewrite minPolyxx big_nil hornerC oner_eq0.
+suff leq_pm : (p <= size s)%N.
+  move: mEx; suff /eqP -> : s == enum 'I_p by [].
+  by rewrite -(geq_leqif (size_subseq_leqif _)) ?mask_subseq// size_enum_ord.
+have /polyOverP/(_ (size s).-1%N) := minPolyOver E x; rewrite {}mEx.
+rewrite -(size_map (fun i => x + (val i)%:R)).
+rewrite coefPn_prod_XsubC size_map -?lt0n// big_map.
+rewrite memvN big_split/= big_const_seq count_predT iter_addr_0 => DE.
+have sE: \sum_(i <- s) i%:R \in E by apply: rpred_sum => i _; apply: rpred_nat.
+move: (rpredB DE sE) => {DE} {sE}.
+rewrite -addrA subrr addr0 => xsE.
+apply/negP => sltp.
+have /coprimeP: coprime (size s) p.
+  rewrite coprime_sym (prime_coprime _ pprim).
+  by apply/negP => /(dvdn_leq smp_gt0).
+move=> /(_ smp_gt0) [[u v]]/= uv1.
+have /ltnW vltu: (v * p < u * size s)%N by rewrite ltnNge -subn_eq0 uv1.
+move: uv1 => /eqP; rewrite -(eqn_add2l (v * p)) addnBA// addnC -addnBA//.
+rewrite subnn addn0 => /eqP sE.
+move: xsE => /(rpredMn u).
+rewrite -mulrnA mulnC sE addn1 mulrS mulrnA -mulr_natr.
+move: p0 => /eqP ->; rewrite mulr0 addr0.
+by move: xE => /negP.
+Qed.
+
+End ArtinSchreier.
+
diff --git a/theories/xmathcomp/map_gal.v b/theories/xmathcomp/map_gal.v
index 10f8600..9febe38 100644
--- a/theories/xmathcomp/map_gal.v
+++ b/theories/xmathcomp/map_gal.v
@@ -19,8 +19,6 @@ Import AEnd_FinGroup.
 Variables (F0 : fieldType) (L : splittingFieldType F0).
 Implicit Types (K E F : {subfield L}).
 
-Lemma galois_subW E F : galois E F -> (E <= F)%VS. Proof. by case/andP. Qed.
-
 Lemma galois_normalW E F : galois E F -> (normalField E F)%VS.
 Proof. by case/and3P. Qed.
 
@@ -37,9 +35,6 @@ Hint Resolve normalField_refl : core.
 Lemma galois_refl E : galois E E.
 Proof. by rewrite /galois subvv separable_refl normalField_refl. Qed.
 
-Lemma gal1 K (g : gal_of K) : g \in 'Gal(K / 1%VS)%g.
-Proof. by rewrite gal_kHom ?sub1v// k1HomE ahomWin. Qed.
-
 Lemma Fadjoin_sub E x y : x \in <<E; y>>%VS -> (<<E; x>> <= <<E; y>>)%VS.
 Proof. by move=> xEy; apply/FadjoinP; rewrite subv_adjoin. Qed.
 
diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v
index d4057eb..888ce1c 100644
--- a/theories/xmathcomp/various.v
+++ b/theories/xmathcomp/various.v
@@ -68,6 +68,11 @@ Lemma big_rcons (R : Type) (idx : R) (op : Monoid.law idx) (I : Type)
   op (\big[op/idx]_(j <- r | P j) F j) (if P i then F i else idx).
 Proof. by rewrite big_rcons_idx -big_change_idx Monoid.mulm1. Qed.
 
+Lemma big_setT [R : Type] [idx : R] (op : Monoid.com_law idx)
+    [I : finType] (F : I -> R) :
+    \big[op/idx]_(i in [set: I]) F i = \big[op/idx]_i F i.
+Proof. by under eq_bigl do rewrite inE. Qed.
+
 (********)
 (* path *)
 (********)
@@ -80,6 +85,14 @@ apply: (iffP andP) => [[ryz rzs] [|i]// /IHs->//|rS].
 by rewrite (rS 0); split=> //; apply/IHs => i /(rS i.+1).
 Qed.
 
+(*******)
+(* div *)
+(*******)
+
+Lemma muln_div_trans (d m n : nat) : (d %| m)%N -> (n %| d)%N ->
+  ((m %/ d) * (d %/ n))%N = (m %/ n)%N.
+Proof. by move=> dm nd; rewrite muln_divA// divnK. Qed.
+
 (*********)
 (* tuple *)
 (*********)
@@ -87,6 +100,10 @@ Qed.
 Section tnth_shift.
 Context {T : Type} {n1 n2} (t1 : n1.-tuple T) (t2 : n2.-tuple T).
 
+Lemma tnth_cons (x : T) (l : seq T) (i : 'I_(size l)) :
+  tnth (in_tuple (x :: l)) (lift ord0 i) = tnth (in_tuple l) i.
+Proof. by rewrite /tnth/=; apply/set_nth_default. Qed.
+
 Lemma tnth_lshift i : tnth [tuple of t1 ++ t2] (lshift n2 i) = tnth t1 i.
 Proof.
 have x0 := tnth_default t1 i; rewrite !(tnth_nth x0).
@@ -100,6 +117,15 @@ by rewrite nth_cat size_tuple ltnNge leq_addr /= addKn.
 Qed.
 End tnth_shift.
 
+(**********)
+(* finfun *)
+(**********)
+
+Lemma ffun_sum [T : finType] [R : ringType] [E : vectType R]
+  (f : seq {ffun T -> E}) (x : T) :
+  ((\sum_(i <- f) i) x = \sum_(i <- f) i x)%R.
+Proof. by elim/big_rec2: _ => [|? ? ? ? <-]; rewrite ffunE. Qed.
+
 (*********)
 (* prime *)
 (*********)
@@ -135,10 +161,69 @@ case: (logn 2 n) => [|[|k]]// ->.
 by rewrite totient_pfactor//= expnS mul1n leq_pmulr ?expn_gt0.
 Qed.
 
+Lemma primes_dvdn (m n : nat) :
+  (0 < n)%N -> (m %| n)%N -> primes m = [seq p <- primes n | p \in primes m].
+Proof.
+move=> n0 mn; apply/(irr_sorted_eq ltn_trans ltnn (sorted_primes _)).
+  by rewrite sorted_filter ?sorted_primes//; apply: ltn_trans.
+move=> p; rewrite mem_filter; case: (boolP (_ \in _)) => //.
+rewrite !mem_primes => /and3P[p_prime m_gt0 dvd_pm]/=.
+by rewrite p_prime n0//= (dvdn_trans dvd_pm).
+Qed.
+
+Lemma dvdn_leq_logP (m n : nat) : (0 < m)%N -> (0 < n)%N ->
+  reflect (forall p, prime p -> logn p m <= logn p n)%N (m %| n)%N.
+Proof.
+move=> m0 n0; apply/(iffP idP) => [mn p prim | vp_le]; first exact/dvdn_leq_log.
+apply/dvdn_partP => // p /[!(inE, mem_primes)]/and3P[p_prime _ pm].
+by rewrite p_part pfactor_dvdn// vp_le.
+Qed.
+
+Lemma logn_prod [I : Type] (r : seq I) (P : pred I) (F : I -> nat) (p : nat) :
+  (forall n,  P n -> (0 < F n)%N) ->
+  (logn p (\prod_(n <- r | P n) F n) = \sum_(n <- r | P n) logn p (F n))%N.
+Proof.
+move=> F_gt0; elim/(big_load (fun n => (n > 0)%N)): _.
+elim/big_rec2: _; first by rewrite logn1.
+by move=> i m n Pi [n_gt0 <-]; rewrite muln_gt0 lognM ?F_gt0.
+Qed.
+
+Lemma logn_partn (p n : nat) (pi : nat_pred) :
+  logn p (n`_pi)%N = ((p \in pi) * logn p n)%N.
+Proof.
+have [p_prime|pNprime] := boolP (prime p); last first.
+  by rewrite /logn !ifN// muln0.
+have [ppi|pNpi] := boolP (p \in pi); last first.
+  by rewrite mul0n logn_coprime// (@p'nat_coprime pi) ?part_pnat// pnatE.
+by rewrite mul1n -logn_part partn_part ?logn_part// => i /eqP->.
+Qed.
+
 (********************)
 (* package fingroup *)
 (********************)
 
+(************)
+(* fingroup *)
+(************)
+
+Lemma cycle_imset [gT : finGroupType] (g : gT) :
+  (<[g]> = [set g ^+ i | i : 'I_#[g]])%g.
+Proof.
+apply/eqP; rewrite eqEsubset; apply/andP; split; apply/subsetP => x.
+   move=> /cycleP [i ->]; apply/imsetP.
+   exists (Ordinal (ltn_pmod i (order_gt0 g))); rewrite ?in_setT//.
+   by rewrite expg_mod_order.
+by move=> /imsetP [i] _ ->; apply/cycleP; exists i.
+Qed.
+
+Lemma cycle_imset_inj [gT : finGroupType] (g : gT) :
+  injective (fun i : 'I_#[g] => g ^+ i)%g.
+Proof.
+move=> [i ilt] [j jlt] /eqP; rewrite eq_expg_mod_order.
+rewrite modn_small// modn_small// => /eqP ijE.
+by apply/val_inj.
+Qed.
+
 (*************)
 (* gproduct? *)
 (*************)
@@ -280,6 +365,37 @@ rewrite pfactor_dvdn// ltn_geF// -[k]muln1 logn_Gauss ?logn1//.
 by rewrite logn_gt0 mem_primes p_prime dvdpn n_gt0.
 Qed.
 
+Lemma memv_mulr_2closed [K : fieldType] [aT : FalgType K] (U : {aspace aT}) :
+  GRing.mulr_2closed U.
+Proof.
+move: U => [U]/[dup]/andP[_ /subvP UU] Ualg.
+by move=> u v uU vU; apply/UU/memv_mul.
+Qed.
+
+Lemma natf_partn_ne0 (R : idomainType) n :
+  (n`_[char R]^')%:R != 0 :> R.
+Proof.
+have n_gt0 := (part_gt0 [char R]^' n).
+apply/negP; rewrite /partn natr_prod prodf_seq_eq0 => /hasP [i] i0n.
+rewrite unfold_in/= natrX expf_eq0 logn_gt0 mem_primes => /andP[/negP ichar].
+move=> /andP[/andP[iprim _] i0]; apply/ichar; rewrite unfold_in/=.
+by apply/andP.
+Qed.
+
+Lemma natf0_partn (R : idomainType) n : (0 < n)%N ->
+  (n%:R == 0 :> R) = (n`_[char R] != 1)%N.
+Proof.
+move=> n_gt0.
+apply/idP/idP => [n0 |].
+   apply/negP => /eqP nchar1.
+   move: n0; rewrite -(partnC [char R] n_gt0) nchar1 mul1n => n0.
+   by move: (natf_partn_ne0 R n); rewrite n0.
+rewrite partn_eq1// /pnat n_gt0/= => /allPn [p].
+rewrite mem_primes => /andP [pprim /andP [_ pn]].
+rewrite /negn/mem/= 2!unfold_in negbK /= => pchar.
+by rewrite -(dvdn_charf pchar).
+Qed.
+
 (**********)
 (* ssrnum *)
 (**********)
@@ -296,6 +412,21 @@ by move=> x xreal; rewrite conj_Creal.
 Qed.
 End ssrnum.
 
+(*********)
+(* zmodp *)
+(*********)
+
+Lemma ZprI p (F : fieldType) : p \in [char F] ->
+   injective (GRing.natmul 1 : 'I_p -> F).
+Proof.
+move=> pchar i j; wlog leij : i j / (j <= i)%N => [hwlog|].
+   by have [/hwlog/[apply]//|/ltnW/hwlog+/esym] := leqP j i => /[apply].
+move=> /eqP; rewrite -subr_eq0 -mulrnBr// -(dvdn_charf pchar) => /eqP ijMp0.
+apply/eqP; rewrite -val_eqE eqn_leq/= leij andbT -subn_eq0.
+rewrite (divn_eq (i - j) p) ijMp0 addn0 divn_small// ltn_subLR//.
+by rewrite (@leq_trans p)// leq_addl.
+Qed.
+
 (**********)
 (* ssrint *)
 (**********)
@@ -352,6 +483,14 @@ Lemma poly_XnsubC_over {R : ringType} n c (S : {pred R}) (addS : subringPred S)
   (kS : keyed_pred addS): c \in kS -> 'X^n - c%:P \is a polyOver kS.
 Proof. by move=> cS; rewrite rpredB ?rpredX ?polyOverX ?polyOverC. Qed.
 
+Lemma polyOver_mulr_2closed [R : ringType] [S : {pred R}]
+  [addS : addrPred S] (kS : keyed_pred addS) :
+  GRing.mulr_2closed kS -> GRing.mulr_2closed (polyOver kS).
+Proof.
+move=> SM u vz /polyOverP uS /polyOverP vS; apply/polyOverP => i.
+by rewrite coefM rpred_sum // => j _; apply/SM.
+Qed.
+
 Lemma lead_coef_prod {R : idomainType} (ps : seq {poly R}) :
   lead_coef (\prod_(p <- ps) p) = \prod_(p <- ps) lead_coef p.
 Proof. by apply/big_morph/lead_coef1; apply: lead_coefM. Qed.
@@ -655,6 +794,44 @@ Qed.
 (* fieldext *)
 (************)
 
+Lemma muln_dimv [F0 : fieldType] [L : fieldExtType F0] (E F K : {subfield L}) :
+  (K <= E)%VS -> (E <= F)%VS -> (\dim_K E * \dim_E F)%N = \dim_K F.
+Proof. by move=> KE EF; rewrite mulnC muln_div_trans// ?field_dimS. Qed.
+
+Lemma ahom_eq_adjoin [F0 : fieldType] [K : fieldExtType F0] [rT : FalgType F0]
+  (f g : 'AHom(K, rT)) (U : {subfield K}) (x : K) :
+  {in U, f =1 g} -> f x = g x -> {in <<U; x>>%VS, f =1 g}.
+Proof.
+move=> fgU fgx y /Fadjoin_poly_eq <-.
+move: (Fadjoin_poly U x y) (Fadjoin_polyOver U x y) => p /polyOverP pU.
+rewrite -(coefK p) horner_poly 2!rmorph_sum/=; apply/eq_bigr => i _.
+by rewrite 2!rmorphM /= fgU// 2!rmorphX/= fgx.
+Qed.
+
+Lemma ahom_eq_adjoin_seq [F0 : fieldType] [K : fieldExtType F0]
+  [rT : FalgType F0] (f g : 'AHom(K, rT)) (U : {aspace K}) (xs : seq K) :
+  {in U, f =1 g} -> {in xs, forall x, f x = g x} -> {in <<U & xs>>%VS, f =1 g}.
+Proof.
+elim: xs U => [|x xs IHxs] U fgU fgxs.
+   by rewrite adjoin_nil subfield_closed.
+rewrite adjoin_cons.
+have ->: <<U; x>>%VS = ASpace (agenv_is_aspace <<U; x>>%VS)
+  by rewrite /= agenv_id.
+move: fgxs (IHxs (ASpace (agenv_is_aspace <<U; x>>))) => fgxs /=.
+rewrite agenv_id; apply.
+   by apply/ahom_eq_adjoin/fgxs => //; apply/mem_head.
+by move=> a axs; apply/fgxs; rewrite in_cons axs orbT.
+Qed.
+
+Lemma agenv_span (K : fieldType) (L : fieldExtType K) (U : {subfield L})
+  (X : seq L) : <<X>>%VS = U -> <<1%VS & X>>%VS = U.
+Proof.
+move=> ->.
+suff ->: (1+U)%VS = U by rewrite subfield_closed.
+rewrite -{2}(subfield_closed U) (agenvEr U) subfield_closed.
+by congr (1 + _)%VS; apply/esym/field_module_eq; rewrite sup_field_module.
+Qed.
+
 Lemma dim_aimg (F : fieldType) (L L' : fieldExtType F) (iota : 'AHom(L, L'))
   (E : {subfield L}) : \dim (iota @: E) = \dim E.
 Proof.
@@ -985,6 +1162,172 @@ have := EF; rewrite rs'E -aimg_adjoin_seq => /eqP.
 by rewrite eq_limg_ker0 ?AHom_lker0// => /eqP.
 Qed.
 
+(**********)
+(* galois *)
+(**********)
+
+Lemma galX (F0 : fieldType) (L : splittingFieldType F0) (E : {subfield L})
+  n (x : gal_of E) [a : L] : a \in E -> (x ^+ n)%g a = iter n x a.
+Proof.
+by elim: n => [|n IHn] aE; rewrite (expg0, expgSr)/= (gal_id, galM)/= ?IHn.
+Qed.
+
+Lemma gal1 (F0 : fieldType) (L : splittingFieldType F0)
+  (K : {subfield L}) (g : gal_of K) : g \in 'Gal(K / 1%VS)%g.
+Proof. by rewrite gal_kHom ?sub1v// k1HomE ahomWin. Qed.
+
+Lemma gal_ne (F0 : fieldType) (L : splittingFieldType F0) (E : {subfield L})
+  (f g : gal_of E) : f = g \/ exists x, x \in E /\ f x != g x.
+Proof.
+move: (vbasisP E) => /span_basis/agenv_span LE.
+case /boolP: (all (fun x => f x == g x) (vbasis E))
+  => [/allP fgE | /allPn[x] xE fgx]; [ left | right ].
+   2: by exists x; split => //; apply/vbasis_mem.
+apply/eqP/gal_eqP.
+rewrite -{1}LE; apply/ahom_eq_adjoin_seq => //; last by move=> x /fgE/eqP.
+move: (gal1 f)(gal1 g).
+rewrite gal_kHom ?sub1v// gal_kHom ?sub1v//.
+move=> /andP [_ /subvP f1] /andP [_ /subvP g1].
+by move=> x /[dup] /f1/fixedSpaceP -> /g1/fixedSpaceP ->.
+Qed.
+
+Lemma gal_free (F0 : fieldType) (L : splittingFieldType F0)
+  (E : {subfield L}) (f : seq (gal_of E)) (k : 'I_(size f) -> L) :
+  uniq f ->
+  (forall i, k i = 0) \/
+    (exists a, a \in E /\ \sum_(i < size f) k i * tnth (in_tuple f) i a != 0).
+Proof.
+move: {1}(size f) (Logic.eq_refl (size f)) => n.
+elim: n f k => [|n IHn] f k fsize funiq.
+   by left; case; move: k; rewrite -fsize.
+case: f => [|s f] in k fsize funiq * => //.
+case: f => [|s0 f] in k fsize funiq * => //.
+   case /boolP: (k 0 == 0).
+      move=> /eqP k0; left => i.
+      by move: k0; congr (k _ = 0); apply/val_inj; case i; case.
+   move=> /negPf k0; right; exists 1; rewrite big_ord1 /= rmorph1; split.
+      by apply/mem1v.
+   by apply/negP; rewrite mulr1 k0.
+move: funiq; rewrite /= negb_or.
+move=> /andP [/andP[ss0 sf]] /[dup] s0f /andP[_ funiq].
+case: (gal_ne s s0) => [/eqP ss0E | [x [xE /negPf ss0x]]].
+   by move: ss0; rewrite ss0E.
+move: fsize => /eqP; rewrite eqSS => /eqP fsize.
+case: (IHn [:: s0 & f]
+  (fun i => (k (lift ord0 i) * (tnth (in_tuple [:: s0 & f]) i x - s x)))
+  fsize s0f).
+   move=> /(_ ord0)/=/eqP.
+   rewrite mulf_eq0 subr_eq0 [s0 x == _]eq_sym ss0x orbF => k10.
+   set k' := fun i : 'I_(size f).+1 => k
+      (match splitP (i : 'I_(1 + size f)%N) with
+      | SplitLo _ _ => ord0
+      | SplitHi _ _ => lift ord0 i
+      end).
+   move: (IHn [:: s & f] k' fsize).
+   have /[swap]/[apply]: uniq (s :: f) by apply/andP; split.
+   case => [k0 | [a [aE fne0]]]; [left => i | right; exists a].
+      case: i; case.
+         move: (k0 ord0); rewrite /k'.
+         by case: splitP => // + _ + ilt => _; congr (k _ = 0); apply/val_inj.
+      case => [|i] ilt.
+         by move: k10 => /eqP; congr (k _ = 0); apply/val_inj.
+      have ile: (i.+1 < (size f).+1)%N by rewrite -ltnS.
+      move: (k0 (Ordinal ile)); rewrite /k'.
+      case: splitP => [[j]/=/[swap]<-// | /= _ _].
+      by congr (k _ = 0); apply/val_inj.
+   split => //.
+   move: k10 fne0 => /eqP k10.
+   rewrite 3!big_ord_recl/= k10 mul0r add0r.
+   congr (_ * _ + _ != 0).
+      by rewrite /k'; case: splitP => // [[i]] /=/(congr1 val).
+   apply/eq_bigr => i _.
+   rewrite tnth_cons (@tnth_cons _ s (s0 :: f) (lift ord0 i)) tnth_cons.
+   congr (_ * _).
+      by rewrite /k'; case: splitP => // [[j]]/=/[swap]<-.
+move=> [y [yE fne0]]; right.
+case /boolP:
+  (\sum_(i < (size f).+2) k i * tnth (in_tuple [:: s, s0 & f]) i y == 0)
+  => [| yne0]; last by exists y.
+rewrite big_ord_recl/= addrC addr_eq0 {2}/tnth/= => /eqP.
+under eq_bigr do rewrite (@tnth_cons _ s (s0 :: f)); move=> y0.
+exists (x*y); split; first by apply/rpredM.
+move: fne0; congr (_ != 0).
+under [\sum_(_ < (size f).+1) _]eq_bigr do rewrite mulrBr mulrBl
+  [X in _ - X * _]mulrC -mulrA -rmorphM/= -[X in _ - X]mulrA.
+rewrite sumrB -mulr_sumr y0 mulrN mulrA opprK [s x * _]mulrC -mulrA -rmorphM/=.
+rewrite addrC [in RHS]big_ord_recl {2}/tnth/=.
+by under [in RHS]eq_bigr do rewrite (@tnth_cons _ s (s0 :: f)).
+Qed.
+
+Lemma galTrace_neq0 (F : fieldType) (L : splittingFieldType F)
+  (K E : {subfield L}) : exists a, a \in E /\ galTrace K E a != 0.
+Proof.
+set l := enum [set: gal_of E].
+have [] := gal_free
+  (fun i : 'I_(size l) => (tnth (in_tuple l) i \in 'Gal(E / K)%G)%:R%:A)
+  (enum_uniq _).
+   have /[dup] l1 : 1%g \in l by rewrite mem_enum.
+   rewrite -index_mem => lt1 /(_ (Ordinal lt1))/=/eqP.
+   by rewrite /tnth (nth_index _ l1) group1/= scaler_eq0 2!oner_eq0.
+move=> [x [xE s0]]; exists x; split => //.
+move: s0; congr (_ != 0); rewrite /galTrace.
+rewrite -(big_tuple _ _ _ xpredT (fun f => (f \in galoisG E K)%:R%:A * f x))/=.
+rewrite /l [in RHS]big_mkcond/= big_enum /= big_setT; apply/eq_bigr => i _.
+case: (i \in galoisG E K) => /=; first by rewrite mulr1n scale1r mul1r.
+by rewrite mulr0n scale0r mul0r.
+Qed.
+
+Lemma galois_subW (F0 : fieldType) (L : splittingFieldType F0)
+  (E F : {subfield L}) : galois E F -> (E <= F)%VS.
+Proof. by case/andP. Qed.
+
+Lemma Hilbert's_theorem_90_additive
+  [F : fieldType] [L : splittingFieldType F]
+    [K E : {subfield L}] [x : gal_of E]
+    [a : L] :
+  galois K E ->
+  generator 'Gal(E / K) x ->
+  a \in E ->
+  reflect (exists2 b : L, b \in E & a = b - x b)
+    (galTrace K E a == 0).
+Proof.
+move=> Egal /eqP DgalE Ea.
+have galEx: x \in 'Gal(E / K)%g by rewrite DgalE cycle_id.
+apply: (iffP eqP) => [normEa0 | [b Eb ->]]; last first.
+   by rewrite raddfB/= galTrace_gal// subrr.
+have [b [bE tb]] := galTrace_neq0 K E.
+move Heqn : (\dim_K E) => n.
+have ordx: #[x]%g = n by rewrite orderE -DgalE -(galois_dim Egal).
+have xXn : (x ^+ n = 1)%g by rewrite -ordx orderE expg_order.
+move: (Egal) => /galois_subW/field_dimS/ltn_divRL/[dup]/(_ 0%N).
+rewrite mul0n adim_gt0 => dimgt0 /(_ 1%N); rewrite mul1n => dimgt1.
+case: n => [|n] in Heqn ordx xXn *; first by move: dimgt0; rewrite Heqn.
+have trE d : d \in E -> galTrace K E d = \sum_(0 <= i < n.+1) (x ^+ i)%g d.
+   move=> dE; rewrite /galTrace DgalE cycle_imset => /=.
+   by rewrite (big_imset _ (in2W (@cycle_imset_inj _ x))) /= ordx big_mkord.
+have trI d : d \in E -> \sum_(0 <= i < n) (x ^+ i.+1)%g d = galTrace K E d - d.
+  by move=> dE; rewrite trE// [in RHS]big_nat_recl//= expg0 gal_id addrC addKr.
+pose c : L := (galTrace K E b)^-1
+  * \sum_(0 <= i < n) (\sum_(0 <= j < i.+1) (x ^+ j)%g a) * (x ^+ i.+1)%g b.
+have tr_b_E : galTrace K E b \in E by rewrite rpred_sum// => * /[!memv_gal].
+exists c.
+   rewrite rpredM// ?rpredV// ?rpred_sum// => i _.
+   by rewrite rpredM//= ?memv_gal// rpred_sum// => j _; rewrite memv_gal.
+rewrite rmorphM/= rmorphV/= ?unitfE//.
+rewrite (fixedFieldP _ (galTrace_fixedField K bE))// -mulrBr rmorph_sum/=.
+pose f i := (\sum_(1 <= j < i.+1) (x ^+ j)%g a) * (x ^+ i.+1)%g b.
+have := @telescope_sumr _ 0 n f isT.
+rewrite /f (@big_geq _ _ _ 1 1)// mul0r subr0 sumrB => /(canRL (addrK _)).
+rewrite big_add1/= trI// normEa0 sub0r opprK addrC.
+under eq_bigr => i.
+  rewrite big_add1; under eq_bigr => j do rewrite expgSr galM//.
+  by rewrite expgSr galM// -rmorph_sum/= -rmorphM /=; over.
+move->; rewrite opprD addrA -sumrB xXn gal_id mulNr opprK.
+under eq_bigr do rewrite big_nat_recl// expg0 gal_id big_add1/= mulrDl addrK.
+by rewrite -mulr_sumr trI// mulrBr addrNK mulrCA mulVf ?mulr1.
+Qed.
+
+
 (********************)
 (* package solvable *)
 (********************)
@@ -1174,3 +1517,104 @@ Lemma solvable_SymF : 4 < #|T| -> solvable 'Sym_T = false.
 Proof. by rewrite (series_sol (Alt_normal T)) => /solvable_AltF->. Qed.
 
 End Perm_solvable.
+
+Section Coef_root_relations.
+
+Lemma big_if (R : Type) (idx : R) (op : Monoid.com_law idx) (I : Type)
+  (r : seq I) (P Q : pred I) (F G : I -> R) :
+  \big[op/idx]_(i <- r | P i) (if Q i then F i else G i) =
+  op (\big[op/idx]_(i <- r | P i && Q i) F i)
+     (\big[op/idx]_(i <- r | P i && ~~ Q i) G i).
+Proof.
+elim: r => [| a r IHr]; first by rewrite 3!big_nil Monoid.mulm1.
+rewrite 3!big_cons.
+case: (P a) => //=.
+case: (Q a) => /=; first by rewrite IHr Monoid.mulmA.
+by rewrite IHr Monoid.mulmCA.
+Qed.
+
+Lemma bigA_distr_bigA2 (R : Type) (zero one : R) (times : Monoid.mul_law zero)
+  (plus : Monoid.add_law zero times) (I : finType) (F G : I -> R) :
+  \big[times/one]_i plus (F i) (G i) =
+  \big[plus/zero]_(J in {set I}) \big[times/one]_i (if i \in J then F i else G i).
+Proof.
+transitivity (\big[times/one]_i \big[plus/zero]_(b : bool) if b then F i else G i); first by apply: eq_bigr => i _; rewrite big_bool.
+rewrite bigA_distr_bigA.
+set f := fun J : {set I} => val J.
+transitivity (\big[plus/zero]_(f0 in (imset f (mem setT))) \big[times/one]_i (if f0 i then F i else G i)).
+  suff <-: setT = imset f (mem setT) by apply: congr_big=>// i; rewrite in_setT.
+  apply/esym/eqP; rewrite -subTset; apply/subsetP => b _.
+  by apply/imsetP; exists (FinSet b).
+rewrite big_imset; last by case => g; case => h _ _; rewrite /f/= => ->.
+apply: congr_big=>//; case => g; first by rewrite in_setT.
+move=>_; apply: eq_bigr => i _; congr (if _ then _ else _).
+by rewrite SetDef.pred_of_setE.
+Qed.
+
+Lemma coefn_prod_XsubC {R : comRingType} (ps : seq R) (n : nat) :
+  (n <= size ps)%N ->
+  (\prod_(p <- ps) ('X - p%:P))`_n =
+  (-1) ^+ (size ps - n)%N *
+    \sum_(I in {set 'I_(size ps)} | #|I| == (size ps - n)%N)
+        \prod_(i in I) ps`_i.
+Proof.
+move=> nle.
+have psE: ps = tval (Tuple (eqxx (size ps))) by [].
+transitivity (\prod_(p <- ps) ((- p)%:P + 'X))`_n.
+  by congr ((polyseq _)`_n); apply: eq_bigr => i _; rewrite addrC polyCN.
+rewrite {1}psE -(map_tnth_enum (Tuple _)) big_map enumT bigA_distr_bigA2 /=.
+rewrite coef_sum.
+transitivity (\sum_(I in {set 'I_(size ps)}) if #|I| == (size ps - n)%N then \prod_(i < size ps | i \in I) - (tnth (Tuple (eqxx (size ps))) i) else 0).
+  apply: eq_bigr => I _.
+  rewrite big_if/= big_const iter_mulr_1.
+  rewrite -(rmorph_prod (@polyC_rmorphism R))/= coefCM coefXn.
+  rewrite -[#|I| == _](eqn_add2l n) addnBA// [(_ + (size ps))%N]addnC -addnBA// subnn addn0 [(n + _)%N]addnC.
+  rewrite -[in X in _ = if _ == X then _ else _](card_ord (size ps)) -(cardC I) eqn_add2l.
+  by case: (n == #|[predC I]|); rewrite ?mulr1 ?mulr0.
+rewrite -big_mkcond mulr_sumr/=; apply: eq_bigr => I /eqP cardI.
+rewrite prodrN cardI; congr GRing.mul; apply: eq_bigr => i _.
+by rewrite (tnth_nth (GRing.zero R)) -psE.
+Qed.
+
+Lemma coefPn_prod_XsubC {R : comRingType} (ps : seq R) :
+  size ps != 0%N ->
+  (\prod_(p <- ps) ('X - p%:P))`_((size ps).-1) =
+  - \sum_(p <- ps) p.
+Proof.
+rewrite coefn_prod_XsubC ?leq_pred// => ps0.
+have ->: (size ps - (size ps).-1 = 1)%N.
+  by move: ps0; case: (size ps)=>// n _; apply: subSnn.
+rewrite expr1 mulN1r; congr GRing.opp.
+set f : 'I_(size ps) -> {set 'I_(size ps)} := fun a => [set a].
+transitivity (\sum_(I in imset f (mem setT)) \prod_(i in I) ps`_i).
+  apply: congr_big=>// I /=.
+  apply/cards1P/imsetP.
+    by move=>[a ->]; exists a.
+  by move=>[a _ ->]; exists a.
+rewrite big_imset/=; last by move=> i j _ _; rewrite/f => ij; apply/set1P; rewrite -ij set11.
+have psE: ps = tval (Tuple (eqxx (size ps))) by [].
+rewrite [in RHS]psE -(map_tnth_enum (Tuple _)) big_map enumT.
+apply: congr_big => // i; first by rewrite in_setT.
+by move=>_; rewrite big_set1 (tnth_nth (GRing.zero R)) -psE.
+Qed.
+
+Lemma coefP0_prod_XsubC {R : comRingType} (ps : seq R) :
+  (\prod_(p <- ps) ('X - p%:P))`_0 =
+  (-1) ^+ (size ps) * \prod_(p <- ps) p.
+Proof.
+rewrite coefn_prod_XsubC// subn0; congr GRing.mul.
+transitivity (\sum_(I in [set setT : {set 'I_(size ps)}]) \prod_(i in I) ps`_i).
+  apply: congr_big=>// i/=.
+  apply/idP/set1P.
+    by move=>/eqP cardE; apply/eqP; rewrite eqEcard subsetT cardsT card_ord cardE leqnn.
+  by move=>->; rewrite cardsT card_ord.
+rewrite big_set1.
+have psE: ps = tval (Tuple (eqxx (size ps))) by [].
+rewrite [in RHS]psE -(map_tnth_enum (Tuple _)) big_map enumT.
+apply: congr_big => // i; first by rewrite in_setT.
+by move=>_; rewrite (tnth_nth (GRing.zero R)) -psE.
+Qed.
+
+
+End Coef_root_relations.
+