moving countalg and closed_field around

- countalg goes to the algebra package
- finalg now get the expected inheritance from countalg
- closed_field now contains the construction of algebraic closure for countable fields (previously in countalg)
- proof of quantifier elimination for closed field rewritten in a monadic style

16 files changed, 692 insertions, 625 deletions

diff --git a/ChangeLog b/ChangeLog
index 2e8a495..c651b13 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -3,6 +3,15 @@
 	* Added companion matrix of a polynomial `companionmx p` and the
 	  theorems: companionmxK, map_mx_companion and companion_map_poly
 
+	* Reshuffled theorems inside files and packages:
+	  * countalg goes from the field to the algebra package
+	  * finalg now gets inheritance from countalg
+	  * closed_field now contains the construction of algebraic closure
+	    for countable fields that used to be in countalg.
+
+        * Rewritten proof of quantifier elimination for closed field in a
+	  monadic style.
+
 	* Added allsigs, the dependent version of allpairs,
 	  with notation `[seq E | i <- s & j <- t]`
 
diff --git a/mathcomp/Make b/mathcomp/Make
index 865234c..df99405 100644
--- a/mathcomp/Make
+++ b/mathcomp/Make
@@ -1,5 +1,6 @@
 algebra/all_algebra.v
 algebra/finalg.v
+algebra/countalg.v
 algebra/fraction.v
 algebra/intdiv.v
 algebra/interval.v
@@ -30,7 +31,6 @@ field/algebraics_fundamentals.v
 field/algnum.v
 field/all_field.v
 field/closed_field.v
-field/countalg.v
 field/cyclotomic.v
 field/falgebra.v
 field/fieldext.v
diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make
index 7d12cb4..b3001f9 100644
--- a/mathcomp/algebra/Make
+++ b/mathcomp/algebra/Make
@@ -1,4 +1,5 @@
 all_algebra.v
+countalg.v
 finalg.v
 fraction.v
 intdiv.v
diff --git a/mathcomp/algebra/all_algebra.v b/mathcomp/algebra/all_algebra.v
index 8a31d60..a937b0c 100644
--- a/mathcomp/algebra/all_algebra.v
+++ b/mathcomp/algebra/all_algebra.v
@@ -1,6 +1,7 @@
 Require Export ssralg.
 Require Export ssrnum.
 Require Export finalg.
+Require Export countalg.
 Require Export poly.
 Require Export polydiv.
 Require Export polyXY.
diff --git a/mathcomp/field/countalg.v b/mathcomp/algebra/countalg.v
index a6d11b3..21000e4 100644
--- a/mathcomp/field/countalg.v
+++ b/mathcomp/algebra/countalg.v
@@ -4,11 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
 From mathcomp
-Require Import bigop ssralg finalg zmodp matrix mxalgebra.
-From mathcomp
-Require Import poly polydiv mxpoly generic_quotient ring_quotient closed_field.
-From mathcomp
-Require Import ssrint rat.
+Require Import bigop ssralg generic_quotient ring_quotient.
 
 (*****************************************************************************)
 (* This file clones part of ssralg hierachy for countable types; it does not *)
@@ -27,7 +23,7 @@ Require Import ssrint rat.
 (*                           zmodType and countType structures.              *)
 (*                    ... etc                                                *)
 (* This file provides constructions for both simple extension and algebraic  *)
-(* closure of countable fields.                                              *) 
+(* closure of countable fields.                                              *)
 (*****************************************************************************)
 
 Set Implicit Arguments.
@@ -798,319 +794,4 @@ End CountRing.
 Import CountRing.
 Export Zmodule.Exports Ring.Exports ComRing.Exports UnitRing.Exports.
 Export ComUnitRing.Exports IntegralDomain.Exports.
-Export Field.Exports DecidableField.Exports ClosedField.Exports.
-
-From mathcomp
-Require Import poly polydiv generic_quotient ring_quotient.
-From mathcomp
-Require Import mxpoly polyXY.
-Import GRing.Theory.
-From mathcomp
-Require Import closed_field.
-
-Canonical Zp_countZmodType m := [countZmodType of 'I_m.+1].
-Canonical Zp_countRingType m := [countRingType of 'I_m.+2].
-Canonical Zp_countComRingType m := [countComRingType of 'I_m.+2].
-Canonical Zp_countUnitRingType m := [countUnitRingType of 'I_m.+2].
-Canonical Zp_countComUnitRingType m := [countComUnitRingType of 'I_m.+2].
-Canonical Fp_countIdomainType p := [countIdomainType of 'F_p].
-Canonical Fp_countFieldType p := [countFieldType of 'F_p].
-Canonical Fp_countDecFieldType p := [countDecFieldType of 'F_p].
-
-Canonical matrix_countZmodType (M : countZmodType) m n :=
-  [countZmodType of 'M[M]_(m, n)].
-Canonical matrix_countRingType (R : countRingType) n :=
-  [countRingType of 'M[R]_n.+1].
-Canonical matrix_countUnitRingType (R : countComUnitRingType) n :=
-  [countUnitRingType of 'M[R]_n.+1].
-
-Definition poly_countMixin (R : countRingType) :=
-  [countMixin of polynomial R by <:].
-Canonical polynomial_countType R := CountType _ (poly_countMixin R).
-Canonical poly_countType (R : countRingType) := [countType of {poly R}].
-Canonical polynomial_countZmodType (R : countRingType) :=
-  [countZmodType of polynomial R].
-Canonical poly_countZmodType (R : countRingType) := [countZmodType of {poly R}].
-Canonical polynomial_countRingType (R : countRingType) :=
-  [countRingType of polynomial R].
-Canonical poly_countRingType (R : countRingType) := [countRingType of {poly R}].
-Canonical polynomial_countComRingType (R : countComRingType) :=
-  [countComRingType of polynomial R].
-Canonical poly_countComRingType (R : countComRingType) :=
-  [countComRingType of {poly R}].
-Canonical polynomial_countUnitRingType (R : countIdomainType) :=
-  [countUnitRingType of polynomial R].
-Canonical poly_countUnitRingType (R : countIdomainType) :=
-  [countUnitRingType of {poly R}].
-Canonical polynomial_countComUnitRingType (R : countIdomainType) :=
-  [countComUnitRingType of polynomial R].
-Canonical poly_countComUnitRingType (R : countIdomainType) :=
-  [countComUnitRingType of {poly R}].
-Canonical polynomial_countIdomainType (R : countIdomainType) :=
-  [countIdomainType of polynomial R].
-Canonical poly_countIdomainType (R : countIdomainType) :=
-  [countIdomainType of {poly R}].
-
-Canonical int_countZmodType := [countZmodType of int].
-Canonical int_countRingType := [countRingType of int].
-Canonical int_countComRingType := [countComRingType of int].
-Canonical int_countUnitRingType := [countUnitRingType of int].
-Canonical int_countComUnitRingType := [countComUnitRingType of int].
-Canonical int_countIdomainType := [countIdomainType of int].
-
-Canonical rat_countZmodType := [countZmodType of rat].
-Canonical rat_countRingType := [countRingType of rat].
-Canonical rat_countComRingType := [countComRingType of rat].
-Canonical rat_countUnitRingType := [countUnitRingType of rat].
-Canonical rat_countComUnitRingType := [countComUnitRingType of rat].
-Canonical rat_countIdomainType := [countIdomainType of rat].
-Canonical rat_countFieldType := [countFieldType of rat].
-
-Lemma countable_field_extension (F : countFieldType) (p : {poly F}) :
-    size p > 1 ->
-  {E : countFieldType & {FtoE : {rmorphism F -> E} &
-  {w : E | root (map_poly FtoE p) w
-         & forall u : E, exists q, u = (map_poly FtoE q).[w]}}}.
-Proof.
-pose fix d i :=
-  if i is i1.+1 then
-    let d1 := oapp (gcdp (d i1)) 0 (unpickle i1) in
-    if size d1 > 1 then d1 else d i1
-  else p.
-move=> p_gt1; have sz_d i: size (d i) > 1 by elim: i => //= i IHi; case: ifP.
-have dv_d i j: i <= j -> d j %| d i.
-  move/subnK <-; elim: {j}(j - i)%N => //= j IHj; case: ifP => //=.
-  case: (unpickle _) => /= [q _|]; last by rewrite size_poly0.
-  exact: dvdp_trans (dvdp_gcdl _ _) IHj.
-pose I : pred {poly F} := [pred q | d (pickle q).+1 %| q].
-have I'co q i: q \notin I -> i > pickle q -> coprimep q (d i).
-  rewrite inE => I'q /dv_d/coprimep_dvdl-> //; apply: contraR I'q.
-  rewrite coprimep_sym /coprimep /= pickleK /= neq_ltn.
-  case: ifP => [_ _| ->]; first exact: dvdp_gcdr.
-  rewrite orbF ltnS leqn0 size_poly_eq0 gcdp_eq0 -size_poly_eq0.
-  by rewrite -leqn0 leqNgt ltnW //.
-have memI q: reflect (exists i, d i %| q) (q \in I).
-  apply: (iffP idP) => [|[i dv_di_q]]; first by exists (pickle q).+1.
-  have [le_i_q | /I'co i_co_q] := leqP i (pickle q).
-    rewrite inE /= pickleK /=; case: ifP => _; first exact: dvdp_gcdr.
-    exact: dvdp_trans (dv_d _ _ le_i_q) dv_di_q.
-  apply: contraR i_co_q _.
-  by rewrite /coprimep (eqp_size (dvdp_gcd_idr dv_di_q)) neq_ltn sz_d orbT.
-have I_ideal : idealr_closed I.
-  split=> [||a q1 q2 Iq1 Iq2]; first exact: dvdp0.
-    by apply/memI=> [[i /idPn[]]]; rewrite dvdp1 neq_ltn sz_d orbT.
-  apply/memI; exists (maxn (pickle q1).+1 (pickle q2).+1); apply: dvdp_add.
-    by apply: dvdp_mull; apply: dvdp_trans Iq1; apply/dv_d/leq_maxl.
-  by apply: dvdp_trans Iq2; apply/dv_d/leq_maxr.
-pose Iaddkey := GRing.Pred.Add (DefaultPredKey I) I_ideal.
-pose Iidkey := MkIdeal (GRing.Pred.Zmod Iaddkey I_ideal) I_ideal.
-pose E := ComRingType _ (@Quotient.mulqC _ _ _ (KeyedPred Iidkey)).
-pose PtoE : {rmorphism {poly F} -> E} := [rmorphism of \pi_E%qT : {poly F} -> E].
-have PtoEd i: PtoE (d i) = 0.
-  by apply/eqP; rewrite piE Quotient.equivE subr0; apply/memI; exists i.
-pose Einv (z : E) (q := repr z) (dq := d (pickle q).+1) :=
-  let q_unitP := Bezout_eq1_coprimepP q dq in
-  if q_unitP is ReflectT ex_uv then PtoE (sval (sig_eqW ex_uv)).1 else 0.
-have Einv0: Einv 0 = 0.
-  rewrite /Einv; case: Bezout_eq1_coprimepP => // ex_uv.
-  case/negP: (oner_neq0 E); rewrite piE -[_ 1]/(PtoE 1); have [uv <-] := ex_uv.
-  by rewrite rmorphD !rmorphM PtoEd /= reprK !mulr0 addr0.
-have EmulV: GRing.Field.axiom Einv.
-  rewrite /Einv=> z nz_z; case: Bezout_eq1_coprimepP => [ex_uv |]; last first.
-    move/Bezout_eq1_coprimepP; rewrite I'co //.
-    by rewrite piE -{1}[z]reprK -Quotient.idealrBE subr0 in nz_z.
-  apply/eqP; case: sig_eqW => {ex_uv} [uv uv1]; set i := _.+1 in uv1 *.
-  rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE.
-  by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; apply: dvdp_mull.
-pose EringU := [comUnitRingType of UnitRingType _ (FieldUnitMixin EmulV Einv0)].
-have Eunitf := @FieldMixin _ _ EmulV Einv0.
-pose Efield := FieldType (IdomainType EringU (FieldIdomainMixin Eunitf)) Eunitf.
-pose Ecount := CountType Efield (CanCountMixin (@reprK _ _)).
-pose FtoE := [rmorphism of PtoE \o polyC]; pose w : E := PtoE 'X.
-have defPtoE q: (map_poly FtoE q).[w] = PtoE q.
-  by rewrite map_poly_comp horner_map [_.['X]]comp_polyXr.
-exists [countFieldType of Ecount], FtoE, w => [|u].
-  by rewrite /root defPtoE (PtoEd 0%N).
-by exists (repr u); rewrite defPtoE /= reprK.
-Qed.
-
-Lemma countable_algebraic_closure (F : countFieldType) :
-  {K : countClosedFieldType & {FtoK : {rmorphism F -> K} | integralRange FtoK}}.
-Proof.
-pose minXp (R : ringType) (p : {poly R}) := if size p > 1 then p else 'X.
-have minXp_gt1 R p: size (minXp R p) > 1.
-  by rewrite /minXp; case: ifP => // _; rewrite size_polyX.
-have minXpE (R : ringType) (p : {poly R}) : size p > 1 -> minXp R p = p.
-  by rewrite /minXp => ->.
-have ext1 p := countable_field_extension (minXp_gt1 _ p).
-pose ext1fT E p := tag (ext1 E p).
-pose ext1to E p : {rmorphism _ -> ext1fT E p} := tag (tagged (ext1 E p)).
-pose ext1w E p : ext1fT E p := s2val (tagged (tagged (ext1 E p))).
-have ext1root E p: root (map_poly (ext1to E p) (minXp E p)) (ext1w E p).
-  by rewrite /ext1w; case: (tagged (tagged (ext1 E p))).
-have ext1gen E p u: {q | u = (map_poly (ext1to E p) q).[ext1w E p]}.
-  by apply: sig_eqW; rewrite /ext1w; case: (tagged (tagged (ext1 E p))) u.
-pose pExtEnum (E : countFieldType) := nat -> {poly E}.
-pose Ext := {E : countFieldType & pExtEnum E}; pose MkExt : Ext := Tagged _ _.
-pose EtoInc (E : Ext) i := ext1to (tag E) (tagged E i).
-pose incEp E i j :=
-  let v := map_poly (EtoInc E i) (tagged E j) in
-  if decode j is [:: i1; k] then
-    if i1 == i then odflt v (unpickle k) else v
-  else v.
-pose fix E_ i := if i is i1.+1 then MkExt _ (incEp (E_ i1) i1) else MkExt F \0.
-pose E i := tag (E_ i); pose Krep := {i : nat & E i}.
-pose fix toEadd i k : {rmorphism E i -> E (k + i)%N} :=
-  if k is k1.+1 then [rmorphism of EtoInc _ (k1 + i)%N \o toEadd _ _]
-  else [rmorphism of idfun].
-pose toE i j (le_ij : i <= j) :=
-  ecast j {rmorphism E i -> E j} (subnK le_ij) (toEadd i (j - i)%N).
-have toEeq i le_ii: toE i i le_ii =1 id.
-  by rewrite /toE; move: (subnK _); rewrite subnn => ?; rewrite eq_axiomK.
-have toEleS i j leij leiSj z: toE i j.+1 leiSj z = EtoInc _ _ (toE i j leij z).
-  rewrite /toE; move: (j - i)%N {leij leiSj}(subnK _) (subnK _) => k.
-  by case: j /; rewrite (addnK i k.+1) => eq_kk; rewrite [eq_kk]eq_axiomK.
-have toEirr := congr1 ((toE _ _)^~ _) (bool_irrelevance _ _).
-have toEtrans j i k leij lejk leik z:
-  toE i k leik z = toE j k lejk (toE i j leij z).
-- elim: k leik lejk => [|k IHk] leiSk lejSk.
-    by case: j => // in leij lejSk *; rewrite toEeq.
-  have:= lejSk; rewrite {1}leq_eqVlt ltnS => /predU1P[Dk | lejk].
-    by rewrite -Dk in leiSk lejSk *; rewrite toEeq.
-  by have leik := leq_trans leij lejk; rewrite !toEleS -IHk.
-have [leMl leMr] := (leq_maxl, leq_maxr); pose le_max := (leq_max, leqnn, orbT).
-pose pairK (x y : Krep) (m := maxn _ _) :=
-  (toE _ m (leMl _ _) (tagged x), toE _ m (leMr _ _) (tagged y)).
-pose eqKrep x y := prod_curry (@eq_op _) (pairK x y).
-have eqKrefl : reflexive eqKrep by move=> z; apply/eqP; apply: toEirr.
-have eqKsym : symmetric eqKrep.
-  move=> z1 z2; rewrite {1}/eqKrep /= eq_sym; move: (leMl _ _) (leMr _ _).
-  by rewrite maxnC => lez1m lez2m; congr (_ == _); apply: toEirr.
-have eqKtrans : transitive eqKrep.
-  rewrite /eqKrep /= => z2 z1 z3 /eqP eq_z12 /eqP eq_z23.
-  rewrite -(inj_eq (fmorph_inj (toE _ _ (leMr (tag z2) _)))).
-  rewrite -!toEtrans ?le_max // maxnCA maxnA => lez3m lez1m.
-  rewrite {lez1m}(toEtrans (maxn (tag z1) (tag z2))) // {}eq_z12.
-  do [rewrite -toEtrans ?le_max // -maxnA => lez2m] in lez3m *.
-  by rewrite (toEtrans (maxn (tag z2) (tag z3))) // eq_z23 -toEtrans.
-pose K := {eq_quot (EquivRel _  eqKrefl eqKsym eqKtrans)}%qT.
-have cntK : Countable.mixin_of K := CanCountMixin (@reprK _ _).
-pose EtoKrep i (x : E i) : K := \pi%qT (Tagged E x).
-have [EtoK piEtoK]: {EtoK | forall i, EtoKrep i =1 EtoK i} by exists EtoKrep.
-pose FtoK := EtoK 0%N; rewrite {}/EtoKrep in piEtoK.
-have eqEtoK i j x y:
-  toE i _ (leMl i j) x = toE j _ (leMr i j) y -> EtoK i x = EtoK j y.
-- by move/eqP=> eq_xy; rewrite -!piEtoK; apply/eqmodP.
-have toEtoK j i leij x : EtoK j (toE i j leij x) = EtoK i x.
-  by apply: eqEtoK; rewrite -toEtrans.
-have EtoK_0 i: EtoK i 0 = FtoK 0 by apply: eqEtoK; rewrite !rmorph0.
-have EtoK_1 i: EtoK i 1 = FtoK 1 by apply: eqEtoK; rewrite !rmorph1.
-have EtoKeq0 i x: (EtoK i x == FtoK 0) = (x == 0).
-  by rewrite /FtoK -!piEtoK eqmodE /= /eqKrep /= rmorph0 fmorph_eq0.
-have toErepr m i leim x lerm:
-  toE _ m lerm (tagged (repr (EtoK i x))) = toE i m leim x.
-- have: (Tagged E x == repr (EtoK i x) %[mod K])%qT by rewrite reprK piEtoK.
-  rewrite eqmodE /= /eqKrep; case: (repr _) => j y /= in lerm * => /eqP /=.
-  have leijm: maxn i j <= m by rewrite geq_max leim.
-  by move/(congr1 (toE _ _ leijm)); rewrite -!toEtrans.
-pose Kadd (x y : K) := EtoK _ (prod_curry +%R (pairK (repr x) (repr y))).
-pose Kopp (x : K) := EtoK _ (- tagged (repr x)).
-pose Kmul (x y : K) := EtoK _ (prod_curry *%R (pairK (repr x) (repr y))).
-pose Kinv (x : K) := EtoK _ (tagged (repr x))^-1.
-have EtoK_D i: {morph EtoK i : x y / x + y >-> Kadd x y}.
-  move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphD.
-  by rewrite -!toEtrans ?le_max  // => lexm leym; rewrite !toErepr.
-have EtoK_N i: {morph EtoK i : x / - x >-> Kopp x}.
-  by move=> x; apply: eqEtoK; set j := tag _; rewrite !rmorphN toErepr.
-have EtoK_M i: {morph EtoK i : x y / x * y >-> Kmul x y}.
-  move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphM.
-  by rewrite -!toEtrans ?le_max  // => lexm leym; rewrite !toErepr.
-have EtoK_V i: {morph EtoK i : x / x^-1 >-> Kinv x}.
-  by move=> x; apply: eqEtoK; set j := tag _; rewrite !fmorphV toErepr.
-case: {toErepr}I in (Kadd) (Kopp) (Kmul) (Kinv) EtoK_D EtoK_N EtoK_M EtoK_V.
-pose inEi i z := {x : E i | z = EtoK i x}; have KtoE z: {i : nat & inEi i z}.
-  by elim/quotW: z => [[i x] /=]; exists i, x; rewrite piEtoK.
-have inEle i j z: i <= j -> inEi i z -> inEi j z.
-  by move=> leij [x ->]; exists (toE i j leij x); rewrite toEtoK.
-have KtoE2 z1 z2: {i : nat & inEi i z1 & inEi i z2}.
-  have [[i1 Ez1] [i2 Ez2]] := (KtoE z1, KtoE z2).
-  by exists (maxn i1 i2); [apply: inEle Ez1 | apply: inEle Ez2].
-have KtoE3 z1 z2 z3: {i : nat & inEi i z1 & inEi i z2 * inEi i z3}%type.
-  have [[i1 Ez1] [i2 Ez2 Ez3]] := (KtoE z1, KtoE2 z2 z3).
-  by exists (maxn i1 i2); [apply: inEle Ez1 | split; apply: inEle (leMr _ _) _].
-have KaddC: commutative Kadd.
-  by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_D addrC.
-have KaddA: associative Kadd.
-  move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w.
-  by rewrite -!EtoK_D addrA.
-have Kadd0: left_id (FtoK 0) Kadd.
-  by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_0 i) -EtoK_D add0r.
-have KaddN: left_inverse (FtoK 0) Kopp Kadd.
-  by move=> u; have [i [x ->]] := KtoE u; rewrite -EtoK_N -EtoK_D addNr EtoK_0.
-pose Kzmod := ZmodType K (ZmodMixin KaddA KaddC Kadd0 KaddN).
-have KmulC: commutative Kmul.
-  by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_M mulrC.
-have KmulA: @associative Kzmod Kmul.
-  move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w.
-  by rewrite -!EtoK_M mulrA.
-have Kmul1: left_id (FtoK 1) Kmul.
-  by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_1 i) -EtoK_M mul1r.
-have KmulD: left_distributive Kmul Kadd.
-  move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w.
-  by rewrite -!(EtoK_M, EtoK_D) mulrDl.
-have Kone_nz: FtoK 1 != FtoK 0 by rewrite EtoKeq0 oner_neq0.
-pose KringMixin := ComRingMixin KmulA KmulC Kmul1 KmulD Kone_nz.
-pose Kring := ComRingType (RingType Kzmod KringMixin) KmulC.
-have KmulV: @GRing.Field.axiom Kring Kinv.
-  move=> u; have [i [x ->]] := KtoE u; rewrite EtoKeq0 => nz_x.
-  by rewrite -EtoK_V -[_ * _]EtoK_M mulVf ?EtoK_1.
-have Kinv0: Kinv (FtoK 0) = FtoK 0 by rewrite -EtoK_V invr0.
-pose Kuring := [comUnitRingType of UnitRingType _ (FieldUnitMixin KmulV Kinv0)].
-pose KfieldMixin := @FieldMixin _ _ KmulV Kinv0.
-pose Kidomain := IdomainType Kuring (FieldIdomainMixin KfieldMixin).
-pose Kfield := FieldType Kidomain KfieldMixin.
-have EtoKrmorphism i: rmorphism (EtoK i : E i -> Kfield).
-  by do 2?split=> [x y|]; rewrite ?EtoK_D ?EtoK_N ?EtoK_M ?EtoK_1.
-pose EtoKM := RMorphism (EtoKrmorphism _); have EtoK_E: EtoK _ = EtoKM _ by [].
-have toEtoKp := @eq_map_poly _ Kring _ _(toEtoK _ _ _).
-have Kclosed: GRing.ClosedField.axiom Kfield.
-  move=> n pK n_gt0; pose m0 := \max_(i < n) tag (KtoE (pK i)); pose m := m0.+1.
-  have /fin_all_exists[pE DpE] (i : 'I_n): exists y, EtoK m y = pK i.
-    pose u := KtoE (pK i); have leum0: tag u <= m0 by rewrite (bigmax_sup i).
-    by have [y ->] := tagged u; exists (toE _ _ (leqW leum0) y); rewrite toEtoK.
-  pose p := 'X^n - rVpoly (\row_i pE i); pose j := code [:: m0; pickle p].
-  pose pj := tagged (E_ j) j; pose w : E j.+1 := ext1w (E j) pj.
-  have lemj: m <= j by rewrite (allP (ltn_code _)) ?mem_head.
-  exists (EtoKM j.+1 w); apply/eqP; rewrite -subr_eq0; apply/eqP.
-  transitivity (EtoKM j.+1 (map_poly (toE m j.+1 (leqW lemj)) p).[w]).
-    rewrite -horner_map -map_poly_comp toEtoKp EtoK_E; move/EtoKM: w => w.
-    rewrite rmorphB [_ 'X^n]map_polyXn !hornerE hornerXn; congr (_ - _ : Kring).
-    rewrite (@horner_coef_wide _ n) ?size_map_poly ?size_poly //.
-    by apply: eq_bigr => i _; rewrite coef_map coef_rVpoly valK mxE /= DpE.
-  suffices Dpj: map_poly (toE m j lemj) p = pj.
-    apply/eqP; rewrite EtoKeq0 (eq_map_poly (toEleS _ _ _ _)) map_poly_comp Dpj.
-    rewrite -rootE -[pj]minXpE ?ext1root // -Dpj size_map_poly.
-    by rewrite size_addl ?size_polyXn ltnS ?size_opp ?size_poly.
-  rewrite {w}/pj; elim: {-9}j lemj => // k IHk lemSk.
-  move: lemSk (lemSk); rewrite {1}leq_eqVlt ltnS => /predU1P[<- | lemk] lemSk.
-    rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)) map_poly_id //= /incEp.
-    by rewrite codeK eqxx pickleK.
-  rewrite (eq_map_poly (toEleS _ _ _ _)) map_poly_comp {}IHk //= /incEp codeK.
-  by rewrite -if_neg neq_ltn lemk.
-suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}.
-  pose Kdec := DecFieldType Kfield (closed_fields_QEMixin Kclosed).
-  pose KclosedField := ClosedFieldType Kdec Kclosed.
-  by exists [countClosedFieldType of CountType KclosedField cntK].
-exists (EtoKM 0%N) => /= z; have [i [{z}z ->]] := KtoE z.
-suffices{z} /(_ z)[p mon_p]: integralRange (toE 0%N i isT).
-  by rewrite -(fmorph_root (EtoKM i)) -map_poly_comp toEtoKp; exists p.
-rewrite /toE /E; clear - minXp_gt1 ext1root ext1gen.
-move: (i - 0)%N (subnK _) => n; case: i /.
-elim: n => [|n IHn] /= z; first exact: integral_id.
-have{z} [q ->] := ext1gen _ _ z; set pn := tagged (E_ _) _.
-apply: integral_horner.
-  by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph.
-apply: integral_root (ext1root _ _) _.
-  by rewrite map_poly_eq0 -size_poly_gt0 ltnW.
-by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph.
-Qed.
+Export Field.Exports DecidableField.Exports ClosedField.Exports.
\ No newline at end of file
diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v
index 7a1cacf..939cd38 100644
--- a/mathcomp/algebra/finalg.v
+++ b/mathcomp/algebra/finalg.v
@@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
 From mathcomp
-Require Import ssralg finset fingroup morphism perm action.
+Require Import ssralg finset fingroup morphism perm action countalg.
 
 (*****************************************************************************)
 (* This file clones the entire ssralg hierachy for finite types; this allows *)
@@ -136,6 +136,7 @@ Notation "[ 'baseFinGroupType' 'of' R 'for' +%R ]" :=
 Notation "[ 'finGroupType' 'of' R 'for' +%R ]" :=
     (@FinGroup.clone R _ (finGroupType _) id _ id)
   (at level 0, format "[ 'finGroupType'  'of'  R  'for'  +%R ]") : form_scope.
+Canonical countZmodType (T : type) := [countZmodType of T].
 End Exports.
 
 End Zmodule.
@@ -219,6 +220,8 @@ Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Canonical countZmodType (T : type) := [countZmodType of T].
+Canonical countRingType (T : type) := [countRingType of T].
 End Exports.
 
 Section Unit.
@@ -330,6 +333,9 @@ Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Canonical countZmodType (T : type) := [countZmodType of T].
+Canonical countRingType (T : type) := [countRingType of T].
+Canonical countComRingType (T : type) := [countComRingType of T].
 End Exports.
 
 End ComRing.
@@ -407,6 +413,9 @@ Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Canonical countZmodType (T : type) := [countZmodType of T].
+Canonical countRingType (T : type) := [countRingType of T].
+Canonical countUnitRingType (T : type) := [countUnitRingType of T].
 End Exports.
 
 End UnitRing.
@@ -590,6 +599,11 @@ Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Canonical countZmodType (T : type) := [countZmodType of T].
+Canonical countRingType (T : type) := [countRingType of T].
+Canonical countUnitRingType (T : type) := [countUnitRingType of T].
+Canonical countComRingType (T : type) := [countComRingType of T].
+Canonical countComUnitRingType (T : type) := [countComUnitRingType of T].
 End Exports.
 
 End ComUnitRing.
@@ -691,6 +705,12 @@ Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Canonical countZmodType (T : type) := [countZmodType of T].
+Canonical countRingType (T : type) := [countRingType of T].
+Canonical countUnitRingType (T : type) := [countUnitRingType of T].
+Canonical countComRingType (T : type) := [countComRingType of T].
+Canonical countComUnitRingType (T : type) := [countComUnitRingType of T].
+Canonical countIdomainType (T : type) := [countIdomainType of T].
 End Exports.
 
 End IntegralDomain.
@@ -800,6 +820,13 @@ Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Canonical countZmodType (T : type) := [countZmodType of T].
+Canonical countRingType (T : type) := [countRingType of T].
+Canonical countUnitRingType (T : type) := [countUnitRingType of T].
+Canonical countComRingType (T : type) := [countComRingType of T].
+Canonical countComUnitRingType (T : type) := [countComUnitRingType of T].
+Canonical countIdomainType (T : type) := [countIdomainType of T].
+Canonical countFieldType (T : type) := [countFieldType of T].
 End Exports.
 
 End Field.
@@ -871,6 +898,7 @@ Canonical finComUnitRingType.
 Canonical finIdomainType.
 Canonical baseFinGroupType.
 Canonical finGroupType.
+
 End Exports.
 
 End DecField.
@@ -940,6 +968,10 @@ Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Section counttype.
+Variables (R : ringType) (phR : phant R) (T : type phR).
+Canonical countZmodType := [countZmodType of T].
+End counttype.
 End Exports.
 
 End Lmodule.
@@ -1036,6 +1068,11 @@ Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Section counttype.
+Variables (R : GRing.Ring.type) (phR : phant R) (T : type phR).
+Canonical countZmodType := [countZmodType of T].
+Canonical countRingType := [countRingType of T].
+End counttype.
 End Exports.
 
 End Lalgebra.
@@ -1131,18 +1168,23 @@ Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Section counttype.
+Variables (R : GRing.Ring.type) (phR : phant R) (T : type phR).
+Canonical countZmodType := [countZmodType of T].
+Canonical countRingType := [countRingType of T].
+End counttype.
 End Exports.
 
 End Algebra.
 Import Algebra.Exports.
 
 Module UnitAlgebra.
- 
+
 Section ClassDef.
 
 Variable R : unitRingType.
- 
-Record class_of M := 
+
+Record class_of M :=
   Class { base : GRing.UnitAlgebra.class_of R M; mixin : mixin_of M base }.
 Definition base2 M (c : class_of M) := Algebra.Class (mixin c).
 Definition base3 M (c : class_of M) := @UnitRing.Class _ (base c) (mixin c).
@@ -1257,12 +1299,18 @@ Canonical ujoin_finLmodType.
 Canonical ujoin_finLalgType.
 Canonical ujoin_finAlgType.
 Notation finUnitAlgType R := (type (Phant R)).
-Notation "[ 'finUnitAlgType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T) 
+Notation "[ 'finUnitAlgType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T)
   (at level 0, format "[ 'finUnitAlgType'  R  'of'  T ]") : form_scope.
 Canonical baseFinGroupType.
 Canonical finGroupType.
 Canonical join_baseFinGroupType.
 Canonical join_finGroupType.
+Section counttype.
+Variables (R : GRing.UnitRing.type) (phR : phant R) (T : type phR).
+Canonical countZmodType := [countZmodType of T].
+Canonical countRingType := [countRingType of T].
+Canonical countUnitRingType := [countUnitRingType of T].
+End counttype.
 End Exports.
 
 End UnitAlgebra.
@@ -1297,4 +1345,3 @@ Notation "{ 'unit' R }" := (unit_of (Phant R))
 Prenex Implicits FinRing.uval.
 Notation "''U'" := (unit_action _) (at level 8) : action_scope.
 Notation "''U'" := (unit_groupAction _) (at level 8) : groupAction_scope.
-
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index fca25a9..2a701a2 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -6,7 +6,7 @@ Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
 From mathcomp
 Require Import finfun bigop prime binomial ssralg finset fingroup finalg.
 From mathcomp
-Require Import perm zmodp.
+Require Import perm zmodp countalg.
 
 (******************************************************************************)
 (* Basic concrete linear algebra : definition of type for matrices, and all   *)
@@ -2071,6 +2071,10 @@ Proof.
 by apply/matrixP=> k i; rewrite !mxE; apply: eq_bigr => j _; rewrite !mxE.
 Qed.
 
+Canonical matrix_countZmodType (M : countZmodType) m n :=
+  [countZmodType of 'M[M]_(m, n)].
+Canonical matrix_countRingType (R : countRingType) n :=
+  [countRingType of 'M[R]_n.+1].
 Canonical matrix_finLmodType (R : finRingType) m n :=
   [finLmodType R of 'M[R]_(m, n)].
 Canonical matrix_finRingType (R : finRingType) n' :=
@@ -2644,6 +2648,9 @@ End MatrixInv.
 
 Prenex Implicits unitmx invmx.
 
+Canonical matrix_countUnitRingType (R : countComUnitRingType) n :=
+  [countUnitRingType of 'M[R]_n.+1].
+
 (* Finite inversible matrices and the general linear group. *)
 Section FinUnitMatrix.
 
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 0f97bb0..040b3a8 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype.
 From mathcomp
-Require Import bigop ssralg binomial tuple.
+Require Import bigop ssralg countalg binomial tuple.
 
 (******************************************************************************)
 (* This file provides a library for univariate polynomials over ring          *)
@@ -152,6 +152,11 @@ Arguments coefp_head _ _ _%N _%R.
 Notation "{ 'poly' T }" := (poly_of (Phant T)).
 Notation coefp i := (coefp_head tt i).
 
+Definition poly_countMixin (R : countRingType) :=
+  [countMixin of polynomial R by <:].
+Canonical polynomial_countType R := CountType _ (poly_countMixin R).
+Canonical poly_countType (R : countRingType) := [countType of {poly R}].
+
 Section PolynomialTheory.
 
 Variable R : ringType.
@@ -1690,6 +1695,13 @@ Arguments rootPt [R p x].
 Arguments unity_rootP [R n z].
 Arguments polyOverP {R S0 addS kS p}.
 
+Canonical polynomial_countZmodType (R : countRingType) :=
+  [countZmodType of polynomial R].
+Canonical poly_countZmodType (R : countRingType) := [countZmodType of {poly R}].
+Canonical polynomial_countRingType (R : countRingType) :=
+  [countRingType of polynomial R].
+Canonical poly_countRingType (R : countRingType) := [countRingType of {poly R}].
+
 (* Container morphism. *)
 Section MapPoly.
 
@@ -2116,6 +2128,11 @@ Definition derivCE := (derivE, deriv_exp).
 
 End PolynomialComRing.
 
+Canonical polynomial_countComRingType (R : countComRingType) :=
+  [countComRingType of polynomial R].
+Canonical poly_countComRingType (R : countComRingType) :=
+  [countComRingType of {poly R}].
+
 Section PolynomialIdomain.
 
 (* Integral domain structure on poly *)
@@ -2353,6 +2370,19 @@ Proof. by move=> ??; apply: contraTeq => ?; rewrite leqNgt max_poly_roots. Qed.
 
 End PolynomialIdomain.
 
+Canonical polynomial_countUnitRingType (R : countIdomainType) :=
+  [countUnitRingType of polynomial R].
+Canonical poly_countUnitRingType (R : countIdomainType) :=
+  [countUnitRingType of {poly R}].
+Canonical polynomial_countComUnitRingType (R : countIdomainType) :=
+  [countComUnitRingType of polynomial R].
+Canonical poly_countComUnitRingType (R : countIdomainType) :=
+  [countComUnitRingType of {poly R}].
+Canonical polynomial_countIdomainType (R : countIdomainType) :=
+  [countIdomainType of polynomial R].
+Canonical poly_countIdomainType (R : countIdomainType) :=
+  [countIdomainType of {poly R}].
+
 Section MapFieldPoly.
 
 Variables (F : fieldType) (R : ringType) (f : {rmorphism F -> R}).
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index b56bc2a..6015f33 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
 From mathcomp
-Require Import bigop ssralg div ssrnum ssrint.
+Require Import bigop ssralg countalg div ssrnum ssrint.
 
 (******************************************************************************)
 (* This file defines a datatype for rational numbers and equips it with a     *)
@@ -350,6 +350,14 @@ Canonical rat_iDomain :=
   Eval hnf in IdomainType rat (FieldIdomainMixin rat_field_axiom).
 Canonical rat_fieldType := FieldType rat rat_field_axiom.
 
+Canonical rat_countZmodType := [countZmodType of rat].
+Canonical rat_countRingType := [countRingType of rat].
+Canonical rat_countComRingType := [countComRingType of rat].
+Canonical rat_countUnitRingType := [countUnitRingType of rat].
+Canonical rat_countComUnitRingType := [countComUnitRingType of rat].
+Canonical rat_countIdomainType := [countIdomainType of rat].
+Canonical rat_countFieldType := [countFieldType of rat].
+
 Lemma numq_eq0 x : (numq x == 0) = (x == 0).
 Proof.
 rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {x} x k0].
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index f12784b..d0214dd 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp
-Require Import fintype finfun bigop ssralg ssrnum poly.
+Require Import fintype finfun bigop ssralg countalg ssrnum poly.
 Import GRing.Theory Num.Theory.
 
 (******************************************************************************)
@@ -359,6 +359,13 @@ Canonical int_comUnitRing := Eval hnf in [comUnitRingType of int].
 Canonical int_iDomain :=
   Eval hnf in IdomainType int intUnitRing.idomain_axiomz.
 
+Canonical int_countZmodType := [countZmodType of int].
+Canonical int_countRingType := [countRingType of int].
+Canonical int_countComRingType := [countComRingType of int].
+Canonical int_countUnitRingType := [countUnitRingType of int].
+Canonical int_countComUnitRingType := [countComUnitRingType of int].
+Canonical int_countIdomainType := [countIdomainType of int].
+
 Definition absz m := match m with Posz p => p | Negz n => n.+1 end.
 Notation "m - n" :=
   (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v
index f9bdaaa..ba6c1b3 100644
--- a/mathcomp/algebra/zmodp.v
+++ b/mathcomp/algebra/zmodp.v
@@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import ssrfun ssrbool eqtype ssrnat seq div.
 From mathcomp
-Require Import fintype bigop finset prime fingroup ssralg finalg.
+Require Import fintype bigop finset prime fingroup ssralg finalg countalg.
 
 (******************************************************************************)
 (*  Definition of the additive group and ring Zp, represented as 'I_p         *)
@@ -364,3 +364,12 @@ Canonical Fp_decFieldType :=
   Eval hnf in [decFieldType of 'F_p for Fp_finFieldType].
 
 End PrimeField.
+
+Canonical Zp_countZmodType m := [countZmodType of 'I_m.+1].
+Canonical Zp_countRingType m := [countRingType of 'I_m.+2].
+Canonical Zp_countComRingType m := [countComRingType of 'I_m.+2].
+Canonical Zp_countUnitRingType m := [countUnitRingType of 'I_m.+2].
+Canonical Zp_countComUnitRingType m := [countComUnitRingType of 'I_m.+2].
+Canonical Fp_countIdomainType p := [countIdomainType of 'F_p].
+Canonical Fp_countFieldType p := [countFieldType of 'F_p].
+Canonical Fp_countDecFieldType p := [countDecFieldType of 'F_p].
diff --git a/mathcomp/field/Make b/mathcomp/field/Make
index 00aa7a5..b7c3f13 100644
--- a/mathcomp/field/Make
+++ b/mathcomp/field/Make
@@ -3,7 +3,6 @@ algC.v
 algebraics_fundamentals.v
 algnum.v
 closed_field.v
-countalg.v
 cyclotomic.v
 falgebra.v
 fieldext.v
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index f7cb614..aef136a 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -6,7 +6,7 @@ Require Import ssrbool ssrfun ssrnat eqtype seq choice div fintype.
 From mathcomp
 Require Import path bigop finset prime ssralg poly polydiv mxpoly.
 From mathcomp
-Require Import generic_quotient countalg ssrnum ssrint rat intdiv.
+Require Import generic_quotient countalg closed_field ssrnum ssrint rat intdiv.
 From mathcomp
 Require Import algebraics_fundamentals.
 
@@ -400,7 +400,7 @@ rewrite horner_poly rmorph_sum; apply: eq_bigr => k _.
 by rewrite rmorphM rmorphX /= LtoC_K.
 Qed.
 
-Definition decFieldMixin := closed_field.closed_fields_QEMixin closedFieldAxiom.
+Definition decFieldMixin := closed_field_QEMixin closedFieldAxiom.
 Canonical decFieldType := DecFieldType type decFieldMixin.
 Canonical closedFieldType := ClosedFieldType type closedFieldAxiom.
 
diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v
index 3696316..8a65f2b 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -6,7 +6,7 @@ Require Import ssrbool ssrfun ssrnat eqtype seq choice div fintype.
 From mathcomp
 Require Import path tuple bigop finset prime ssralg poly polydiv mxpoly.
 From mathcomp
-Require Import countalg ssrnum ssrint rat intdiv.
+Require Import countalg closed_field ssrnum ssrint rat intdiv.
 From mathcomp
 Require Import fingroup finalg zmodp cyclic pgroup sylow.
 From mathcomp
@@ -27,7 +27,7 @@ Require Import vector falgebra fieldext separable galois.
 (* algebraics as a subfield. To avoid some duplication a few basic properties *)
 (* of the algebraics, such as the existence of minimal polynomials, that are  *)
 (* required by the proof of the Theorem, are also proved here.                *)
-(*  The main theorem of countalg.v supplies us directly with an algebraic     *)
+(*  The main theorem of closed_field supplies us directly with an algebraic   *)
 (* closure of the rationals (as the rationals are a countable field), so all  *)
 (* we really need to construct is a conjugation automorphism that exchanges   *)
 (* the two roots (i and -i) of X^2 + 1, and fixes a (real) subfield of        *)
diff --git a/mathcomp/field/all_field.v b/mathcomp/field/all_field.v
index a57ac19..2641bbe 100644
--- a/mathcomp/field/all_field.v
+++ b/mathcomp/field/all_field.v
@@ -2,7 +2,6 @@ Require Export algC.
 Require Export algebraics_fundamentals.
 Require Export algnum.
 Require Export closed_field.
-Require Export countalg.
 Require Export cyclotomic.
 Require Export falgebra.
 Require Export fieldext.
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index 5c57df8..1ae025b 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -2,94 +2,143 @@
 (* Distributed under the terms of CeCILL-B.                                  *)
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat seq.
+Require Import ssrfun ssrbool eqtype choice ssrnat seq fintype generic_quotient.
 From mathcomp
-Require Import bigop ssralg poly polydiv.
+Require Import bigop ssralg poly polydiv matrix mxpoly countalg ring_quotient.
 
 (******************************************************************************)
-(*   A proof that algebraically closed field enjoy quantifier elimination,    *)
-(*   as described in                                                          *)
-(*   ``A formal quantifier elimination for algebraically closed fields'',     *)
-(*    proceedings of Calculemus 2010, by Cyril Cohen and Assia Mahboubi       *)
+(* This files contains two main contributions:                                *)
+(* 1. Theorem "closed_field_QEMixin"                                          *)
+(*    A proof that algebraically closed field enjoy quantifier elimination,   *)
+(*    as described in                                                         *)
+(*    ``A formal quantifier elimination for algebraically closed fields'',    *)
+(*     proceedings of Calculemus 2010, by Cyril Cohen and Assia Mahboubi      *)
 (*                                                                            *)
-(* This file constructs an instance of quantifier elimination mixin,          *)
+(* We constructs an instance of quantifier elimination mixin,                 *)
 (* (see the ssralg library) from the theory of polynomials with coefficients  *)
 (* is an algebraically closed field (see the polydiv library).                *)
+(* The algebraic operations operating on fomulae are implemented in CPS style *)
+(* We provide one CPS counterpart for each operation involved in the proof    *)
+(* of quantifier elimination. See the paper  for more details.                *)
 (*                                                                            *)
-(* This file hence deals with the transformation of formulae part, which we   *)
-(* address by implementing one CPS style formula transformer per effective    *)
-(* operation involved in the proof of quantifier elimination. See the paper   *)
-(* for more details.                                                          *)
+(* 2. Theorems "countable_field_extension" and "countable_algebraic_closure"  *)
+(*    constructions for both simple extension and algebraic closure of        *)
+(*    countable fields, by Georges Gonthier.                                  *)
+(*    Note that the construction of the algebraic closure relies on the       *)
+(*    above mentionned quantifier elimination.                                *)
 (******************************************************************************)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-Import GRing.
+Import GRing.Theory.
 Local Open Scope ring_scope.
 
 Import Pdiv.Ring.
 Import PreClosedField.
 
+Module ClosedFieldQE.
 Section ClosedFieldQE.
 
-Variable F : Field.type.
+Variables (F : fieldType) (F_closed : GRing.ClosedField.axiom F).
 
-Variable axiom : ClosedField.axiom F.
+Notation fF := (@GRing.formula F).
+Notation tF := (@GRing.term F).
+Notation qf f := (GRing.qf_form f && GRing.rformula f).
+Definition polyF := seq tF.
 
-Notation fF := (formula F).
-Notation qf f := (qf_form f && rformula f).
+Lemma qf_simpl (f : fF) :
+  (qf f -> GRing.qf_form f) * (qf f -> GRing.rformula f).
+Proof. by split=> /andP[]. Qed.
 
-Definition polyF := seq (term F).
+Notation cps T := ((T -> fF) -> fF).
+Definition ret T1 : T1 -> cps T1 := fun x k => k x.
+Arguments ret T1 x k /.
 
-Fixpoint eval_poly (e : seq F) pf := 
-  if pf is c::q then (eval_poly e q)*'X + (eval e c)%:P else 0.
+Definition bind T1 T2 (x : cps T1) (f : T1 -> cps T2) : cps T2 :=
+  fun k => x (fun x => f x k).
+Arguments bind T1 T2 x f k /.
+Notation "''let' x <- y ; z" :=
+  (bind y (fun x => z)) (at level 99, x at level 0, y at level 0,
+    format "'[hv' ''let'  x  <-  y ;  '/' z ']'").
+
+Definition cpsif T (c : fF) (t : T) (e : T) : cps T :=
+  fun k => GRing.If c (k t) (k e).
+Arguments cpsif T c t e k /.
+Notation "''if' c1 'then' c2 'else' c3" := (cpsif c1%T c2%T c3%T)
+  (at level 200, right associativity, format
+"'[hv   ' ''if'  c1  '/' '[' 'then'  c2  ']' '/' '[' 'else'  c3 ']' ']'").
+
+Notation eval := GRing.eval.
+Notation rterm := GRing.rterm.
+Notation qf_eval := GRing.qf_eval.
+
+Fixpoint eval_poly (e : seq F) pf :=
+  if pf is c :: q then eval_poly e q * 'X + (eval e c)%:P else 0.
 
 Definition rpoly (p : polyF) := all (@rterm F) p.
 
-Fixpoint sizeT (k : nat -> fF) (p : polyF) :=
-  if p is c::q then 
-    sizeT (fun n => 
-      if n is m.+1 then k m.+2 else 
-        GRing.If (c == 0) (k 0%N) (k 1%N)) q 
-   else k O%N.
+Definition sizeT : polyF -> cps nat := (fix loop p :=
+  if p isn't c :: q then ret 0%N
+  else 'let n <- loop q;
+       if n is m.+1 then ret m.+2 else
+       'if (c == 0) then 0%N else 1%N).
+
+Definition qf_red_cps T (x : cps T) (y : _ -> T) :=
+   forall e k, qf_eval e (x k) = qf_eval e (k (y e)).
+Notation "x ->_ e y" := (qf_red_cps x (fun e => y))
+  (e ident, at level 90, format "x  ->_ e  y").
 
+Definition qf_cps T D (x : cps T) :=
+  forall k, (forall y, D y -> qf (k y)) -> qf (x k).
 
-Lemma sizeTP (k : nat -> formula F) (pf : polyF) (e : seq F) : 
-  qf_eval e (sizeT k pf) = qf_eval e (k (size (eval_poly e pf))).
+Lemma qf_cps_ret T D (x : T) : D x -> qf_cps D (ret x).
+Proof. move=> ??; exact. Qed.
+Hint Resolve qf_cps_ret.
+
+Lemma qf_cps_bind T1 D1 T2 D2 (x : cps T1) (f : T1 -> cps T2) :
+  qf_cps D1 x -> (forall x, D1 x -> qf_cps D2 (f x)) -> qf_cps D2 (bind x f).
+Proof. by move=> xP fP k kP /=; apply: xP => y ?; apply: fP. Qed.
+
+Lemma qf_cps_if T D (c : fF) (t : T) (e : T) : qf c -> D t -> D e ->
+  qf_cps D ('if c then t else e).
 Proof.
-elim: pf e k; first by move=> *; rewrite size_poly0.
-move=> c qf Pqf e k; rewrite Pqf.
-rewrite size_MXaddC -(size_poly_eq0 (eval_poly _ _)).
+move=> qfc Dt De k kP /=; have [qft qfe] := (kP _ Dt, kP _ De).
+by do !rewrite qf_simpl //.
+Qed.
+
+Lemma sizeTP (pf : polyF) : sizeT pf ->_e size (eval_poly e pf).
+Proof.
+elim: pf=> [|c qf qfP /=]; first by rewrite /= size_poly0.
+move=> e k; rewrite size_MXaddC qfP -(size_poly_eq0 (eval_poly _ _)).
 by case: (size (eval_poly e qf))=> //=; case: eqP; rewrite // orbF.
 Qed.
 
-Lemma sizeT_qf (k : nat -> formula F) (p : polyF) : 
-  (forall n, qf (k n)) -> rpoly p -> qf (sizeT k p).
+Lemma sizeT_qf (p : polyF) : rpoly p -> qf_cps xpredT (sizeT p).
 Proof.
-elim: p k => /= [|c q ihp] k kP rp; first exact: kP.
-case/andP: rp=> rc rq.
-apply: ihp; rewrite ?rq //; case=> [|n]; last exact: kP.
-have [/andP[qf0 rf0] /andP[qf1 rf1]] := (kP 0, kP 1)%N.
-by rewrite If_form_qf ?If_form_rf //= andbT.
+elim: p => /= [_|c p ihp /andP[rc rq]]; first exact: qf_cps_ret.
+apply: qf_cps_bind; first exact: ihp.
+move=> [|n] //= _; last exact: qf_cps_ret.
+by apply: qf_cps_if; rewrite //= rc.
 Qed.
 
-Definition isnull (k : bool -> fF) (p : polyF) :=
-  sizeT (fun n => k (n == 0%N)) p.
+Definition isnull (p : polyF) : cps bool :=
+  'let n <- sizeT p; ret (n == 0%N).
 
-Lemma isnullP (k : bool -> formula F) (p : polyF) (e : seq F) :
-  qf_eval e (isnull k p) = qf_eval e (k (eval_poly e p == 0)).
-Proof. by rewrite sizeTP size_poly_eq0. Qed.
+Lemma isnullP (p : polyF) : isnull p ->_e (eval_poly e p == 0).
+Proof. by move=> e k; rewrite sizeTP size_poly_eq0. Qed.
 
-Lemma isnull_qf (k : bool -> formula F) (p : polyF) :
-  (forall b, qf (k b)) -> rpoly p -> qf (isnull k p).
-Proof. by move=> *; apply: sizeT_qf. Qed.
+Lemma isnull_qf (p : polyF) : rpoly p -> qf_cps xpredT (isnull p).
+Proof.
+move=> rp; apply: qf_cps_bind; first exact: sizeT_qf.
+by move=> ? _; apply: qf_cps_ret.
+Qed.
 
-Definition lt_sizeT (k : bool -> fF) (p q : polyF) : fF :=
-  sizeT (fun n => sizeT (fun m => k (n<m)) q) p.
+Definition lt_sizeT (p q : polyF) : cps bool :=
+  'let n <- sizeT p; 'let m <- sizeT q; ret (n < m).
 
-Definition lift (p : {poly F}) := let: q := p in map Const q.
+Definition lift (p : {poly F}) := map GRing.Const p.
 
 Lemma eval_lift (e : seq F) (p : {poly F}) : eval_poly e (lift p) = p.
 Proof.
@@ -103,39 +152,38 @@ case c0: (_==_)=> /=.
 by rewrite mul0r add0r; apply: val_inj=> /=; rewrite polyseq_cons // /nilp pn0.
 Qed.
 
-Fixpoint lead_coefT (k : term F -> fF) p :=  
-  if p is c::q then 
-    lead_coefT (fun l => GRing.If (l == 0) (k c) (k l)) q 
-  else k (Const 0).
+Fixpoint lead_coefT p : cps tF :=
+  if p is c :: q then
+    'let l <- lead_coefT q; 'if (l == 0) then c else l
+  else ret 0%T.
 
-Lemma lead_coefTP (k : term F -> formula F) :
- (forall x e, qf_eval e (k x) = qf_eval e (k (Const (eval e x)))) ->
+Lemma lead_coefTP (k : tF -> fF) :
+ (forall x e, qf_eval e (k x) = qf_eval e (k (eval e x)%:T%T)) ->
   forall (p : polyF) (e : seq F),
-  qf_eval e (lead_coefT k p) = qf_eval e (k (Const (lead_coef (eval_poly e p)))).
+  qf_eval e (lead_coefT p k) = qf_eval e (k (lead_coef (eval_poly e p))%:T%T).
 Proof.
-move=> Pk p e; elim: p k Pk => /= [*|a p' Pp' k Pk]; first by rewrite lead_coef0.
-rewrite Pp'; last by move=> *; rewrite //= -Pk.
+move=> kP p e; elim: p => [|a p IHp]/= in k kP e *.
+  by rewrite lead_coef0 kP.
+rewrite IHp; last by move=> *; rewrite //= -kP.
 rewrite GRing.eval_If /= lead_coef_eq0.
-case p'0: (_ == _); first by rewrite (eqP p'0) mul0r add0r lead_coefC -Pk.
+case p'0: (_ == _); first by rewrite (eqP p'0) mul0r add0r lead_coefC -kP.
 rewrite lead_coefDl ?lead_coefMX // polyseqC size_mul ?p'0 //; last first.
   by rewrite -size_poly_eq0 size_polyX.
 rewrite size_polyX addnC /=; case: (_ == _)=> //=.
 by rewrite ltnS lt0n size_poly_eq0 p'0.
 Qed.
 
-Lemma lead_coefT_qf (k : term F -> formula F) (p : polyF) :
- (forall c, rterm c -> qf (k c)) -> rpoly p -> qf (lead_coefT k p).
+Lemma lead_coefT_qf (p : polyF) : rpoly p -> qf_cps (@rterm _) (lead_coefT p).
 Proof.
-elim: p k => /= [|c q ihp] k kP rp; first exact: kP.
-move: rp; case/andP=> rc rq; apply: ihp; rewrite ?rq // => l rl.
-have [/andP[qfc rfc] /andP[qfl rfl]] := (kP c rc, kP l rl).
-by rewrite If_form_qf ?If_form_rf //= andbT.
+elim: p => [_|c q ihp //= /andP[rc rq]]; first by apply: qf_cps_ret.
+apply: qf_cps_bind => [|y ty]; first exact: ihp.
+by apply: qf_cps_if; rewrite //= ty.
 Qed.
 
-Fixpoint amulXnT (a : term F) (n : nat) : polyF :=
-  if n is n'.+1 then (Const 0) :: (amulXnT a n') else [::a].
+Fixpoint amulXnT (a : tF) (n : nat) : polyF :=
+  if n is n'.+1 then 0%T :: (amulXnT a n') else [:: a].
 
-Lemma eval_amulXnT  (a : term F) (n : nat) (e : seq F) :
+Lemma eval_amulXnT  (a : tF) (n : nat) (e : seq F) :
   eval_poly e (amulXnT a n) = (eval e a)%:P * 'X^n.
 Proof.
 elim: n=> [|n] /=; first by rewrite expr0 mulr1 mul0r add0r.
@@ -146,10 +194,8 @@ Lemma ramulXnT: forall a n, rterm a -> rpoly (amulXnT a n).
 Proof. by move=> a n; elim: n a=> [a /= -> //|n ihn a ra]; apply: ihn. Qed.
 
 Fixpoint sumpT (p q : polyF) :=
-  if p is a::p' then
-    if q is b::q' then (Add a b)::(sumpT p' q')
-      else p
-    else q.
+  match p, q with a :: p, b :: q => (a + b)%T :: sumpT p q
+                | [::], q => q | p, [::] => p end.
 
 Lemma eval_sumpT (p q : polyF) (e : seq F) :
   eval_poly e (sumpT p q) = (eval_poly e p) + (eval_poly e q).
@@ -168,7 +214,8 @@ by case/andP=> -> rq //=; apply: ihp.
 Qed.
 
 Fixpoint mulpT (p q : polyF) :=
-  if p is a :: p' then sumpT (map (Mul a) q) (Const 0::(mulpT p' q)) else [::].
+  if p isn't a :: p then [::]
+  else sumpT [seq (a * x)%T | x <- q] (0%T :: mulpT p q).
 
 Lemma eval_mulpT (p q : polyF) (e : seq F) :
   eval_poly e (mulpT p q) = (eval_poly e p) * (eval_poly e q).
@@ -179,8 +226,8 @@ elim: q=> [|b q Hq] /=; first by rewrite mulr0.
 by rewrite Hq polyC_mul mulrDr mulrA.
 Qed.
 
-Lemma rpoly_map_mul (t : term F) (p : polyF) (rt : rterm t) : 
-  rpoly (map (Mul t) p) = rpoly p.
+Lemma rpoly_map_mul (t : tF) (p : polyF) (rt : rterm t) :
+  rpoly [seq (t * x)%T | x <- p] = rpoly p.
 Proof.
 by rewrite /rpoly all_map /= (@eq_all _ _ (@rterm _)) // => x; rewrite /= rt.
 Qed.
@@ -192,15 +239,15 @@ apply: rsumpT; last exact: ihp.
 by rewrite rpoly_map_mul.
 Qed.
 
-Definition opppT := map (Mul (@Const F (-1))).
+Definition opppT : polyF -> polyF := map (GRing.Mul (- 1%T)%T).
 
-Lemma eval_opppT (p : polyF) (e : seq F) : 
- eval_poly e (opppT p) = - eval_poly e p.
+Lemma eval_opppT (p : polyF) (e : seq F) :
+  eval_poly e (opppT p) = - eval_poly e p.
 Proof.
 by elim: p; rewrite /= ?oppr0 // => ? ? ->; rewrite !mulNr opprD polyC_opp mul1r.
 Qed.
 
-Definition natmulpT n := map (Mul (@NatConst F n)).
+Definition natmulpT n : polyF -> polyF := map (GRing.Mul n%:R%T).
 
 Lemma eval_natmulpT  (p : polyF) (n : nat) (e : seq F) :
   eval_poly e (natmulpT n p) = (eval_poly e p) *+ n.
@@ -210,21 +257,19 @@ rewrite mulrnDl mulr_natl polyC_muln; congr (_ + _).
 by rewrite -mulr_natl mulrAC -mulrA mulr_natl mulrC.
 Qed.
 
-Fixpoint redivp_rec_loopT (q : polyF) sq cq (k : nat * polyF * polyF -> fF)
-  (c : nat) (qq r : polyF) (n : nat) {struct n}:=
-  sizeT (fun sr => 
-    if sr < sq then k (c, qq, r) else 
-      lead_coefT (fun lr =>
-        let m := amulXnT lr (sr - sq) in
-        let qq1 := sumpT (mulpT qq [::cq]) m in
-        let r1 := sumpT (mulpT r ([::cq])) (opppT (mulpT m q)) in
-        if n is n1.+1 then redivp_rec_loopT q sq cq k c.+1 qq1 r1 n1
-        else k (c.+1, qq1, r1)
-      ) r
-  ) r.
-  
-Fixpoint redivp_rec_loop (q : {poly F}) sq cq 
-   (k : nat) (qq r : {poly F})(n : nat) {struct n} :=
+Fixpoint redivp_rec_loopT (q : polyF) sq cq (c : nat) (qq r : polyF)
+  (n : nat) {struct n} : cps (nat * polyF * polyF) :=
+  'let sr <- sizeT r;
+  if sr < sq then ret (c, qq, r) else
+  'let lr <- lead_coefT r;
+  let m := amulXnT lr (sr - sq) in
+  let qq1 := sumpT (mulpT qq [::cq]) m in
+  let r1 := sumpT (mulpT r ([::cq])) (opppT (mulpT m q)) in
+  if n is n1.+1 then redivp_rec_loopT q sq cq c.+1 qq1 r1 n1
+  else ret (c.+1, qq1, r1).
+
+Fixpoint redivp_rec_loop (q : {poly F}) sq cq
+   (k : nat) (qq r : {poly F}) (n : nat) {struct n} :=
     if size r < sq then (k, qq, r) else
       let m := (lead_coef r) *: 'X^(size r - sq) in
       let qq1 := qq * cq%:P + m in
@@ -232,13 +277,13 @@ Fixpoint redivp_rec_loop (q : {poly F}) sq cq
       if n is n1.+1 then redivp_rec_loop q sq cq k.+1 qq1 r1 n1 else
         (k.+1, qq1, r1).
 
-Lemma redivp_rec_loopTP (k : nat * polyF * polyF -> formula F) : 
-  (forall c qq r e,  qf_eval e (k (c,qq,r)) 
+Lemma redivp_rec_loopTP (k : nat * polyF * polyF -> fF) :
+  (forall c qq r e,  qf_eval e (k (c,qq,r))
     = qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r))))
-  -> forall q sq cq c qq r n e 
+  -> forall q sq cq c qq r n e
     (d := redivp_rec_loop (eval_poly e q) sq (eval e cq)
       c (eval_poly e qq) (eval_poly e r) n),
-    qf_eval e (redivp_rec_loopT q sq cq k c qq r n) 
+    qf_eval e (redivp_rec_loopT q sq cq c qq r n k)
     = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
 Proof.
 move=> Pk q sq cq c qq r n e /=.
@@ -259,221 +304,192 @@ rewrite Pk ?(eval_lift,eval_mulpT,eval_amulXnT,eval_sumpT,eval_opppT).
 by rewrite mul_polyC ?(mul0r,add0r).
 Qed.
 
-Lemma redivp_rec_loopT_qf (q : polyF) (sq : nat) (cq : term F)
- (k : nat * polyF * polyF -> formula F) (c : nat) (qq r : polyF) (n : nat) :
-  (forall r, [&& rpoly r.1.2 & rpoly r.2] -> qf (k r)) ->
+Lemma redivp_rec_loopT_qf (q : polyF) (sq : nat) (cq : tF)
+  (c : nat) (qq r : polyF) (n : nat) :
   rpoly q -> rterm cq -> rpoly qq -> rpoly r ->
-    qf (redivp_rec_loopT q sq cq k c qq r n).
-Proof.
-elim: n q sq cq k c qq r => [|n ihn] q sq cq k c qq r kP rq rcq rqq rr.
-  apply: sizeT_qf=> // n; case: (_ < _); first by apply: kP; rewrite // rqq rr.
-  apply: lead_coefT_qf=> // l rl; apply: kP.
-  by rewrite /= ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq.
-apply: sizeT_qf=> // m; case: (_ < _); first by apply: kP => //=; rewrite rqq rr.
-apply: lead_coefT_qf=> // l rl; apply: ihn; rewrite //= ?rcq //.
-  by rewrite ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq.
-by rewrite ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul) //= rcq.
-Qed.
-
-Definition redivpT (p : polyF) (k : nat * polyF * polyF -> fF) 
-                   (q : polyF) : fF :=
-  isnull (fun b =>
-    if b then k (0%N, [::Const 0], p) else
-      sizeT (fun sq =>
-        sizeT (fun sp =>
-          lead_coefT (fun lq =>
-            redivp_rec_loopT q sq lq k 0 [::Const 0] p sp
-          ) q
-        ) p
-      ) q
-  ) q.
+  qf_cps (fun x => [&& rpoly x.1.2 & rpoly x.2])
+         (redivp_rec_loopT q sq cq c qq r n).
+Proof.
+do ![move=>x/(pair x){x}] => rw; elim: n => [|n IHn]//= in q sq cq c qq r rw *;
+apply: qf_cps_bind; do ?[by apply: sizeT_qf; rewrite !rw] => sr _;
+case: ifPn => // _; do ?[by apply: qf_cps_ret; rewrite //= ?rw];
+apply: qf_cps_bind; do ?[by apply: lead_coefT_qf; rewrite !rw] => lr /= rlr;
+[apply: qf_cps_ret|apply: IHn];
+by do !rewrite ?(rsumpT,rmulpT,ramulXnT,rpoly_map_mul,rlr,rw) //=.
+Qed.
+
+Definition redivpT (p : polyF) (q : polyF) : cps (nat * polyF * polyF) :=
+  'let b <- isnull q;
+  if b then ret (0%N, [::0%T], p) else
+  'let sq <- sizeT q; 'let sp <- sizeT p;
+  'let lq <- lead_coefT q;
+  redivp_rec_loopT q sq lq 0 [::0%T] p sp.
 
 Lemma redivp_rec_loopP  (q : {poly F}) (c : nat) (qq r : {poly F}) (n : nat) :
   redivp_rec q c qq r n = redivp_rec_loop q (size q) (lead_coef q) c qq r n.
 Proof. by elim: n c qq r => [| n Pn] c qq r //=; rewrite Pn. Qed.
 
-Lemma redivpTP (k : nat * polyF * polyF -> formula F) :
-  (forall c qq r e,  
-     qf_eval e (k (c,qq,r)) = 
+Lemma redivpTP (k : nat * polyF * polyF -> fF) :
+  (forall c qq r e,
+     qf_eval e (k (c,qq,r)) =
      qf_eval e (k (c, lift (eval_poly e qq), lift (eval_poly e r)))) ->
   forall p q e (d := redivp (eval_poly e p) (eval_poly e q)),
-    qf_eval e (redivpT p k q) = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
+    qf_eval e (redivpT p q k) = qf_eval e (k (d.1.1, lift d.1.2, lift d.2)).
 Proof.
-move=> Pk p q e /=; rewrite isnullP unlock.
-case q0 : (_ == _); first by rewrite Pk /= mul0r add0r polyC0.
+move=> Pk p q e /=; rewrite isnullP unlock /=.
+case q0 : (eval_poly e q == 0) => /=; first by rewrite Pk /= mul0r add0r polyC0.
 rewrite !sizeTP lead_coefTP /=; last by move=> *; rewrite !redivp_rec_loopTP.
 rewrite redivp_rec_loopTP /=; last by move=> *; rewrite Pk.
 by rewrite mul0r add0r polyC0 redivp_rec_loopP.
 Qed.
 
-Lemma redivpT_qf (p : polyF) (k : nat * polyF * polyF -> formula F) (q : polyF) :
-  (forall r, [&& rpoly r.1.2 & rpoly r.2] -> qf (k r)) ->
-   rpoly p -> rpoly q -> qf (redivpT p k q).
+Lemma redivpT_qf (p : polyF) (q : polyF) : rpoly p -> rpoly q ->
+  qf_cps (fun x => [&& rpoly x.1.2 & rpoly x.2]) (redivpT p q).
 Proof.
-move=> kP rp rq; rewrite /redivpT; apply: isnull_qf=> // [[]]; first exact: kP.
-apply: sizeT_qf => // sq; apply: sizeT_qf=> // sp.
-by apply: lead_coefT_qf=> // lq rlq; apply: redivp_rec_loopT_qf.
+move=> rp rq; apply: qf_cps_bind => [|[] _]; first exact: isnull_qf.
+  by apply: qf_cps_ret.
+apply: qf_cps_bind => [|sp _]; first exact: sizeT_qf.
+apply: qf_cps_bind => [|sq _]; first exact: sizeT_qf.
+apply: qf_cps_bind => [|lq rlq]; first exact: lead_coefT_qf.
+by apply: redivp_rec_loopT_qf => //=.
 Qed.
 
-Definition rmodpT (p : polyF) (k : polyF -> fF) (q : polyF) : fF :=
-  redivpT p (fun d => k d.2) q.
-Definition rdivpT (p : polyF) (k:polyF -> fF) (q : polyF) : fF :=
-  redivpT p (fun d => k d.1.2) q.
-Definition rscalpT (p : polyF) (k: nat -> fF) (q : polyF) : fF :=
-  redivpT p (fun d => k d.1.1) q.
-Definition rdvdpT (p : polyF) (k:bool -> fF) (q : polyF) : fF :=
-  rmodpT p (isnull k) q.
+Definition rmodpT (p : polyF) (q : polyF) : cps polyF :=
+  'let d <- redivpT p q; ret d.2.
+Definition rdivpT (p : polyF) (q : polyF) : cps polyF :=
+  'let d <- redivpT p q; ret d.1.2.
+Definition rscalpT (p : polyF) (q : polyF) : cps nat :=
+  'let d <- redivpT p q; ret d.1.1.
+Definition rdvdpT (p : polyF) (q : polyF) : cps bool :=
+  'let d <- rmodpT p q; isnull d.
 
 Fixpoint rgcdp_loop n (pp qq : {poly F}) {struct n} :=
-  if rmodp pp qq == 0 then qq 
-    else if n is n1.+1 then rgcdp_loop n1 qq (rmodp pp qq)
-         else rmodp pp qq.
-
-Fixpoint rgcdp_loopT (pp : polyF) (k : polyF -> formula F) n (qq : polyF) :=
-  rmodpT pp (isnull 
-    (fun b => if b then (k qq) 
-              else (if n is n1.+1 
-                    then rmodpT pp (rgcdp_loopT qq k n1) qq 
-                    else rmodpT pp k qq)
-    )
-            ) qq.
-
-Lemma rgcdp_loopP (k : polyF -> formula F) :
+  let rr := rmodp pp qq in if rr == 0 then qq
+    else if n is n1.+1 then rgcdp_loop n1 qq rr else rr.
+
+Fixpoint rgcdp_loopT n (pp : polyF) (qq : polyF) : cps polyF :=
+  'let rr <- rmodpT pp qq; 'let nrr <- isnull rr; if nrr then ret qq
+    else if n is n1.+1 then rgcdp_loopT n1 qq rr else ret rr.
+
+Lemma rgcdp_loopP (k : polyF -> fF) :
   (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) ->
-  forall n p q e, 
-    qf_eval e (rgcdp_loopT p k n q) = 
+  forall n p q e,
+    qf_eval e (rgcdp_loopT n p q k) =
     qf_eval e (k (lift (rgcdp_loop n (eval_poly e p) (eval_poly e q)))).
 Proof.
-move=> Pk n p q e.
-elim: n p q e => /= [| m Pm] p q e.
-  rewrite redivpTP; last by move=> *; rewrite !isnullP eval_lift.
-  rewrite isnullP eval_lift; case: (_ == 0); first by rewrite Pk.
-  by rewrite redivpTP; last by move=> *; rewrite Pk.
-rewrite redivpTP; last by move=> *; rewrite !isnullP eval_lift.
-rewrite isnullP eval_lift; case: (_ == 0); first by rewrite Pk.
-by rewrite redivpTP => *; rewrite ?Pm !eval_lift.
-Qed.
-
-Lemma rgcdp_loopT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) (n : nat) :
-  (forall r, rpoly r -> qf (k r)) -> 
-  rpoly p -> rpoly q -> qf (rgcdp_loopT p k n q).
-elim: n p k q => [|n ihn] p k q kP rp rq.
-  apply: redivpT_qf=> // r; case/andP=> _ rr.
-  apply: isnull_qf=> // [[]]; first exact: kP.
-  by apply: redivpT_qf=> // r'; case/andP=> _ rr'; apply: kP.
-apply: redivpT_qf=> // r; case/andP=> _ rr.
-apply: isnull_qf=> // [[]]; first exact: kP.
-by apply: redivpT_qf=> // r'; case/andP=> _ rr'; apply: ihn.
-Qed.
-   
-Definition rgcdpT (p : polyF) k (q : polyF) : fF :=
-  let aux p1 k q1 := isnull 
-    (fun b => if b 
-      then (k q1) 
-      else (sizeT (fun n => (rgcdp_loopT p1 k n q1)) p1)) p1
-    in (lt_sizeT (fun b => if b then (aux q k p) else (aux p k q)) p q).
-
-Lemma rgcdpTP (k : seq (term F) -> formula F) :
+move=> Pk n p q e; elim: n => /= [| m IHm] in p q e *;
+rewrite redivpTP /==> *; rewrite ?isnullP ?eval_lift -/(rmodp _ _);
+by case: (_ == _); do ?by rewrite -?Pk ?IHm ?eval_lift.
+Qed.
+
+Lemma rgcdp_loopT_qf (n : nat) (p : polyF) (q : polyF) :
+  rpoly p -> rpoly q -> qf_cps rpoly (rgcdp_loopT n p q).
+Proof.
+elim: n => [|n IHn] in p q * => rp rq /=;
+(apply: qf_cps_bind=> [|rr rrr]; [
+  apply: qf_cps_bind => [|[[a u] v]]; do ?exact: redivpT_qf;
+  by move=> /andP[/= ??]; apply: (@qf_cps_ret _ rpoly)|
+apply: qf_cps_bind => [|[] _];
+by [apply: isnull_qf|apply: qf_cps_ret|apply: IHn]]).
+Qed.
+
+Definition rgcdpT (p : polyF) (q : polyF) : cps polyF :=
+  let aux p1 q1 : cps polyF :=
+    'let b <- isnull p1; if b then ret q1
+    else 'let n <- sizeT p1; rgcdp_loopT n p1 q1 in
+  'let b <- lt_sizeT p q; if b then aux q p else aux p q.
+
+Lemma rgcdpTP (k : polyF -> fF) :
   (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) ->
-   forall p q e, qf_eval e (rgcdpT p k q) = 
+   forall p q e, qf_eval e (rgcdpT p q k) =
                  qf_eval e (k (lift (rgcdp (eval_poly e p) (eval_poly e q)))).
 Proof.
-move=> Pk p q e; rewrite /rgcdpT !sizeTP; case lqp: (_ < _).
-  rewrite isnullP; case q0: (_ == _); first by rewrite Pk (eqP q0) rgcdp0.
-  rewrite sizeTP rgcdp_loopP => [|e' p']; last by rewrite Pk.
-  by rewrite /rgcdp lqp q0.
-rewrite isnullP; case p0: (_ == _); first by rewrite Pk (eqP p0) rgcd0p.
-rewrite sizeTP rgcdp_loopP => [|e' p']; last by rewrite Pk.
-by rewrite /rgcdp lqp p0.
+move=> Pk p q e; rewrite /rgcdpT /rgcdp !sizeTP /=.
+case: (_ < _); rewrite !isnullP /=; case: (_ == _); rewrite -?Pk ?sizeTP;
+by rewrite ?rgcdp_loopP.
 Qed.
 
-Lemma rgcdpT_qf  (p : polyF) (k : polyF -> formula F) (q : polyF) :
-  (forall r, rpoly r -> qf (k r)) -> rpoly p -> rpoly q -> qf (rgcdpT p k q).
+Lemma rgcdpT_qf (p : polyF) (q : polyF) :
+   rpoly p -> rpoly q -> qf_cps rpoly (rgcdpT p q).
 Proof.
-move=> kP rp rq; apply: sizeT_qf=> // n; apply: sizeT_qf=> // m.
-by case: (_ < _);
-   apply: isnull_qf=> //; case; do ?apply: kP=> //;
-   apply: sizeT_qf=> // n'; apply: rgcdp_loopT_qf.
+move=> rp rq k kP; rewrite /rgcdpT /=; do ![rewrite sizeT_qf => // ? _].
+case: (_ < _); rewrite ?isnull_qf // => -[]; rewrite ?kP // => _;
+by rewrite sizeT_qf => // ? _; rewrite rgcdp_loopT_qf.
 Qed.
 
-Fixpoint rgcdpTs k (ps : seq polyF) : fF :=
-  if ps is p::pr then rgcdpTs (rgcdpT p k) pr else k [::Const 0].
+Fixpoint rgcdpTs (ps : seq polyF) : cps polyF :=
+  if ps is p :: pr then 'let pr <- rgcdpTs pr; rgcdpT p pr else ret [::0%T].
 
-Lemma rgcdpTsP (k : polyF -> formula F) : 
+Lemma rgcdpTsP (k : polyF -> fF) :
   (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) ->
-  forall ps e, 
-    qf_eval e (rgcdpTs k ps) = 
+  forall ps e,
+    qf_eval e (rgcdpTs ps k) =
     qf_eval e (k (lift (\big[@rgcdp _/0%:P]_(i <- ps)(eval_poly e i)))).
 Proof.
-move=> Pk ps e.
-elim: ps k Pk; first by move=> p Pk; rewrite /= big_nil Pk /= mul0r add0r.
-move=> p ps Pps /= k Pk /=; rewrite big_cons Pps => [|p' e'].
-  by rewrite rgcdpTP // eval_lift.
-by rewrite !rgcdpTP // Pk !eval_lift .
+move=> Pk ps e; elim: ps k Pk => [|p ps Pps] /= k Pk.
+  by rewrite /= big_nil Pk /= mul0r add0r.
+by rewrite big_cons Pps => *; rewrite !rgcdpTP // !eval_lift -?Pk.
 Qed.
 
-Definition rseq_poly ps := all rpoly ps.
-
-Lemma rgcdpTs_qf (k : polyF -> formula F) (ps : seq polyF) :
-  (forall r, rpoly r -> qf (k r)) -> rseq_poly ps -> qf (rgcdpTs k ps).
+Lemma rgcdpTs_qf (ps : seq polyF) :
+   all rpoly ps -> qf_cps rpoly (rgcdpTs ps).
 Proof.
-elim: ps k=> [|c p ihp] k kP rps=> /=; first exact: kP.
-by move: rps; case/andP=> rc rp; apply: ihp=> // r rr; apply: rgcdpT_qf.
+elim: ps => [_|c p ihp /andP[rc rp]] //=; first exact: qf_cps_ret.
+by apply: qf_cps_bind => [|r rr]; [apply: ihp|apply: rgcdpT_qf].
 Qed.
 
-Fixpoint rgdcop_recT (q : polyF) k  (p : polyF) n :=
+Fixpoint rgdcop_recT n (q : polyF) (p : polyF) :=
   if n is m.+1 then
-    rgcdpT p (sizeT (fun sd =>
-      if sd == 1%N then k p
-      else rgcdpT p (rdivpT p (fun r => rgdcop_recT q k r m)) q
-    )) q
-  else isnull (fun b => k [::Const b%:R]) q.
+    'let g <- rgcdpT p q; 'let sg <- sizeT g;
+    if sg == 1%N then ret p
+    else 'let r <- rdivpT p g;
+          rgdcop_recT m q r
+  else 'let b <- isnull q; ret [::b%:R%T].
 
 
-Lemma rgdcop_recTP (k : polyF -> formula F) : 
+Lemma rgdcop_recTP (k : polyF -> fF) :
   (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p))))
-  -> forall p q n e, qf_eval e (rgdcop_recT p k q n) 
+  -> forall p q n e, qf_eval e (rgdcop_recT n p q k)
     = qf_eval e (k (lift (rgdcop_rec (eval_poly e p) (eval_poly e q) n))).
 Proof.
-move=> Pk p q n e.
-elim: n k Pk p q e => [|n Pn] k Pk p q e /=.
+move=> Pk p q n e; elim: n => [|n Pn] /= in k Pk p q e *.
   rewrite isnullP /=.
   by case: (_ == _); rewrite Pk /= mul0r add0r ?(polyC0, polyC1).
-rewrite rgcdpTP ?sizeTP ?eval_lift //.
-  rewrite /rcoprimep; case se : (_==_); rewrite Pk //.
-  do ?[rewrite (rgcdpTP,Pn,eval_lift,redivpTP) | move=> * //=].
-by do ?[rewrite (sizeTP,eval_lift) | move=> * //=].
+rewrite /rcoprimep rgcdpTP ?sizeTP ?eval_lift => * /=.
+  case: (_ == _);
+  by do ?[rewrite /= ?(=^~Pk, redivpTP, rgcdpTP, sizeTP, Pn, eval_lift) //==> *].
+do ?[rewrite /= ?(=^~Pk, redivpTP, rgcdpTP, sizeTP, Pn, eval_lift) //==> *].
+case: (_ == _);
+by do ?[rewrite /= ?(=^~Pk, redivpTP, rgcdpTP, sizeTP, Pn, eval_lift) //==> *].
 Qed.
 
-Lemma rgdcop_recT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) (n : nat) :
- (forall r, rpoly r -> qf (k r)) -> 
- rpoly p -> rpoly q -> qf (rgdcop_recT p k q n).
+Lemma rgdcop_recT_qf (n : nat) (p : polyF) (q : polyF) :
+  rpoly p -> rpoly q -> qf_cps rpoly (rgdcop_recT n p q).
 Proof.
-elim: n p k q => [|n ihn] p k q kP rp rq /=.
-apply: isnull_qf=> //; first by case; rewrite kP.
-apply: rgcdpT_qf=> // g rg; apply: sizeT_qf=> // n'.
-case: (_ == _); first exact: kP.
-apply: rgcdpT_qf=> // g' rg'; apply: redivpT_qf=> // r; case/andP=> rr _.
-exact: ihn.
+elim: n => [|n ihn] in p q * => k kP rp rq /=.
+  by rewrite isnull_qf => //*; rewrite rq.
+rewrite rgcdpT_qf=> //*; rewrite sizeT_qf=> //*.
+case: (_ == _); rewrite ?kP ?rq //= redivpT_qf=> //= ? /andP[??].
+by rewrite ihn.
 Qed.
 
-Definition rgdcopT q k p := sizeT (rgdcop_recT q k p) p.
+Definition rgdcopT q p := 'let sp <- sizeT p; rgdcop_recT sp q p.
 
-Lemma rgdcopTP (k : polyF -> formula F) : 
+Lemma rgdcopTP (k : polyF -> fF) :
   (forall p e, qf_eval e (k p) = qf_eval e (k (lift (eval_poly e p)))) ->
-  forall p q e, qf_eval e (rgdcopT p k q) =
+  forall p q e, qf_eval e (rgdcopT p q k) =
                 qf_eval e (k (lift (rgdcop (eval_poly e p) (eval_poly e q)))).
 Proof. by move=> *; rewrite sizeTP rgdcop_recTP 1?Pk. Qed.
 
-Lemma rgdcopT_qf (p : polyF) (k : polyF -> formula F) (q : polyF) :
-  (forall r, rpoly r -> qf (k r)) -> rpoly p -> rpoly q -> qf (rgdcopT p k q).
+Lemma rgdcopT_qf (p : polyF) (q : polyF) :
+  rpoly p -> rpoly q -> qf_cps rpoly (rgdcopT p q).
 Proof.
-by move=> kP rp rq; apply: sizeT_qf => // n; apply: rgdcop_recT_qf.
+by move=> rp rq k kP; rewrite sizeT_qf => //*; rewrite rgdcop_recT_qf.
 Qed.
 
-
-Definition ex_elim_seq (ps : seq polyF) (q : polyF) :=
-  (rgcdpTs (rgdcopT q (sizeT (fun n => Bool (n != 1%N)))) ps).
+Definition ex_elim_seq (ps : seq polyF) (q : polyF) : fF :=
+  ('let g <- rgcdpTs ps; 'let d <- rgdcopT q g;
+  'let n <- sizeT d; ret (n != 1%N)) GRing.Bool.
 
 Lemma ex_elim_seqP (ps : seq polyF) (q : polyF) (e : seq F) :
   let gp := (\big[@rgcdp _/0%:P]_(p <- ps)(eval_poly e p)) in
@@ -483,25 +499,24 @@ by do ![rewrite (rgcdpTsP,rgdcopTP,sizeTP,eval_lift) //= | move=> * //=].
 Qed.
 
 Lemma ex_elim_seq_qf  (ps : seq polyF) (q : polyF) :
-  rseq_poly ps -> rpoly q -> qf (ex_elim_seq ps q).
+  all rpoly ps -> rpoly q -> qf (ex_elim_seq ps q).
 Proof.
 move=> rps rq; apply: rgcdpTs_qf=> // g rg; apply: rgdcopT_qf=> // d rd.
 exact : sizeT_qf.
 Qed.
 
-Fixpoint abstrX (i : nat) (t : term F) :=
+Fixpoint abstrX (i : nat) (t : tF) :=
   match t with
-    | (Var n) => if n == i then [::Const 0; Const 1] else [::t]
-    | (Opp x) => opppT (abstrX i x)
-    | (Add x y) => sumpT (abstrX i x) (abstrX i y)
-    | (Mul x y) => mulpT (abstrX i x) (abstrX i y)
-    | (NatMul x n) => natmulpT n (abstrX i x)
-    | (Exp x n) => let ax := (abstrX i x) in
-      iter n (mulpT ax) [::Const 1]
+    | 'X_n => if n == i then [::0; 1] else [::t]
+    | - x => opppT (abstrX i x)
+    | x + y => sumpT (abstrX i x) (abstrX i y)
+    | x * y => mulpT (abstrX i x) (abstrX i y)
+    | x *+ n => natmulpT n (abstrX i x)
+    | x ^+ n => let ax := (abstrX i x) in iter n (mulpT ax) [::1]
     | _ => [::t]
-  end.
+  end%T.
 
-Lemma abstrXP  (i : nat) (t : term F) (e : seq F) (x : F) :
+Lemma abstrXP  (i : nat) (t : tF) (e : seq F) (x : F) :
   rterm t -> (eval_poly e (abstrX i t)).[x] = eval (set_nth 0 e i x) t.
 Proof.
 elim: t => [n | r | n | t tP s sP | t tP | t tP n | t tP s sP | t tP | t tP n] h.
@@ -519,7 +534,7 @@ elim: t => [n | r | n | t tP s sP | t tP | t tP n | t tP s sP | t tP | t tP n] h
   by rewrite /= eval_mulpT exprSr hornerM ihn // mulrC tP.
 Qed.
 
-Lemma rabstrX (i : nat) (t : term F) : rterm t -> rpoly (abstrX i t).
+Lemma rabstrX (i : nat) (t : tF) : rterm t -> rpoly (abstrX i t).
 Proof.
 elim: t; do ?[ by move=> * //=; do ?case: (_ == _)].
 - move=> t irt s irs /=; case/andP=> rt rs.
@@ -532,36 +547,36 @@ elim: t; do ?[ by move=> * //=; do ?case: (_ == _)].
   exact: rmulpT.
 Qed.
 
-Implicit Types tx ty : term F.
+Implicit Types tx ty : tF.
 
-Lemma abstrX_mulM (i : nat) : {morph abstrX i : x y / Mul x y >-> mulpT x y}.
-Proof. done. Qed.
+Lemma abstrX_mulM (i : nat) : {morph abstrX i : x y / x * y >-> mulpT x y}%T.
+Proof. by []. Qed.
 
-Lemma abstrX1 (i : nat) : abstrX i (Const 1) = [::Const 1].
+Lemma abstrX1 (i : nat) : abstrX i 1%T = [::1%T].
 Proof. done. Qed.
 
-Lemma eval_poly_mulM e : {morph eval_poly e : x y / mulpT x y >-> mul x y}.
+Lemma eval_poly_mulM e : {morph eval_poly e : x y / mulpT x y >-> x * y}.
 Proof. by move=> x y; rewrite eval_mulpT. Qed.
 
-Lemma eval_poly1 e : eval_poly e [::Const 1] = 1.
+Lemma eval_poly1 e : eval_poly e [::1%T] = 1.
 Proof. by rewrite /= mul0r add0r. Qed.
 
 Notation abstrX_bigmul := (big_morph _ (abstrX_mulM _) (abstrX1 _)).
 Notation eval_bigmul := (big_morph _ (eval_poly_mulM _) (eval_poly1 _)).
 Notation bigmap_id := (big_map _ (fun _ => true) id).
 
-Lemma rseq_poly_map (x : nat) (ts : seq (term F)) :
-  all (@rterm _) ts ->  rseq_poly (map (abstrX x) ts).
+Lemma rseq_poly_map (x : nat) (ts : seq tF) :
+  all (@rterm _) ts ->  all rpoly (map (abstrX x) ts).
 Proof.
 by elim: ts => //= t ts iht; case/andP=> rt rts; rewrite rabstrX // iht.
 Qed.
 
-Definition ex_elim (x : nat) (pqs : seq (term F) * seq (term F)) :=
-  ex_elim_seq (map (abstrX x) pqs.1) 
-  (abstrX x (\big[Mul/Const 1]_(q <- pqs.2) q)).
- 
-Lemma ex_elim_qf (x : nat) (pqs : seq (term F) * seq (term F)) : 
-  dnf_rterm pqs -> qf (ex_elim x pqs).
+Definition ex_elim (x : nat) (pqs : seq tF * seq tF) :=
+  ex_elim_seq (map (abstrX x) pqs.1)
+  (abstrX x (\big[GRing.Mul/1%T]_(q <- pqs.2) q)).
+
+Lemma ex_elim_qf (x : nat) (pqs : seq tF * seq tF) :
+  GRing.dnf_rterm pqs -> qf (ex_elim x pqs).
 case: pqs => ps qs; case/andP=> /= rps rqs.
 apply: ex_elim_seq_qf; first exact: rseq_poly_map.
 apply: rabstrX=> /=.
@@ -570,7 +585,8 @@ by case/andP=> rt rts; rewrite big_cons /= rt /= iht.
 Qed.
 
 Lemma holds_conj : forall e i x ps, all (@rterm _) ps ->
-  (holds (set_nth 0 e i x) (foldr (fun t : term F => And (t == 0)) True ps)
+  (GRing.holds (set_nth 0 e i x)
+               (foldr (fun t : tF => GRing.And (t == 0)) GRing.True%T ps)
   <-> all ((@root _)^~ x) (map (eval_poly e \o abstrX i) ps)).
 Proof.
 move=> e i x; elim=> [|p ps ihps] //=.
@@ -579,9 +595,10 @@ constructor; first by case=> -> hps; rewrite eqxx /=; apply/ihps.
 by case/andP; move/eqP=> -> psr; split=> //; apply/ihps.
 Qed.
 
-Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq (term F)) :
+Lemma holds_conjn (e : seq F) (i : nat) (x : F) (ps : seq tF) :
   all (@rterm _) ps ->
-  (holds (set_nth 0 e i x) (foldr (fun t : term F => And (t != 0)) True ps) <-> 
+  (GRing.holds (set_nth 0 e i x)
+               (foldr (fun t : tF => GRing.And (t != 0)) GRing.True ps) <->
   all (fun p => ~~root p x) (map (eval_poly e \o abstrX i) ps)).
 Proof.
 elim: ps => [|p ps ihps] //=.
@@ -611,12 +628,12 @@ case g0: (\big[(@rgcdp F)/0%:P]_(j <- map (eval_poly e \o abstrX i) ps) j == 0).
     case=> _; move/holds_conjn=> hc; move/hc:rqs.
     by rewrite -root_bigmul //= (eqP m0) root0.
   constructor; move/negP:m0; move/negP=>m0.
-  case: (closed_nonrootP axiom _ m0) => x {m0}.
+  case: (closed_nonrootP F_closed _ m0) => x {m0}.
   rewrite abstrX_bigmul eval_bigmul -bigmap_id root_bigmul=> m0.
   exists x; do 2?constructor=> //; last by apply/holds_conjn.
   apply/holds_conj; rewrite //= -root_biggcd.
   by rewrite (eqp_root (aux _ _ _ )) (eqP g0) root0.
-apply: (iffP (closed_rootP axiom _)); case=> x Px; exists x; move: Px => //=.
+apply: (iffP (closed_rootP F_closed _)) => -[x Px]; exists x; move: Px => //=.
   rewrite (eqp_root (eqp_rgdco_gdco _ _)) root_gdco ?g0 //.
   rewrite -(eqp_root (aux _ _ _ )) root_biggcd  abstrX_bigmul eval_bigmul.
   rewrite -bigmap_id root_bigmul; case/andP=> psr qsr.
@@ -632,7 +649,259 @@ Qed.
 Lemma wf_ex_elim : GRing.wf_QE_proj ex_elim.
 Proof. by move=> i bc /= rbc; apply: ex_elim_qf. Qed.
 
-Definition closed_fields_QEMixin := 
-  QEdecFieldMixin wf_ex_elim holds_ex_elim.
+Definition Mixin := QEdecFieldMixin wf_ex_elim holds_ex_elim.
 
 End ClosedFieldQE.
+End ClosedFieldQE.
+Notation closed_field_QEMixin := ClosedFieldQE.Mixin.
+
+Import CodeSeq.
+
+Lemma countable_field_extension (F : countFieldType) (p : {poly F}) :
+    size p > 1 ->
+  {E : countFieldType & {FtoE : {rmorphism F -> E} &
+  {w : E | root (map_poly FtoE p) w
+         & forall u : E, exists q, u = (map_poly FtoE q).[w]}}}.
+Proof.
+pose fix d i :=
+  if i is i1.+1 then
+    let d1 := oapp (gcdp (d i1)) 0 (unpickle i1) in
+    if size d1 > 1 then d1 else d i1
+  else p.
+move=> p_gt1; have sz_d i: size (d i) > 1 by elim: i => //= i IHi; case: ifP.
+have dv_d i j: i <= j -> d j %| d i.
+  move/subnK <-; elim: {j}(j - i)%N => //= j IHj; case: ifP => //=.
+  case: (unpickle _) => /= [q _|]; last by rewrite size_poly0.
+  exact: dvdp_trans (dvdp_gcdl _ _) IHj.
+pose I : pred {poly F} := [pred q | d (pickle q).+1 %| q].
+have I'co q i: q \notin I -> i > pickle q -> coprimep q (d i).
+  rewrite inE => I'q /dv_d/coprimep_dvdl-> //; apply: contraR I'q.
+  rewrite coprimep_sym /coprimep /= pickleK /= neq_ltn.
+  case: ifP => [_ _| ->]; first exact: dvdp_gcdr.
+  rewrite orbF ltnS leqn0 size_poly_eq0 gcdp_eq0 -size_poly_eq0.
+  by rewrite -leqn0 leqNgt ltnW //.
+have memI q: reflect (exists i, d i %| q) (q \in I).
+  apply: (iffP idP) => [|[i dv_di_q]]; first by exists (pickle q).+1.
+  have [le_i_q | /I'co i_co_q] := leqP i (pickle q).
+    rewrite inE /= pickleK /=; case: ifP => _; first exact: dvdp_gcdr.
+    exact: dvdp_trans (dv_d _ _ le_i_q) dv_di_q.
+  apply: contraR i_co_q _.
+  by rewrite /coprimep (eqp_size (dvdp_gcd_idr dv_di_q)) neq_ltn sz_d orbT.
+have I_ideal : idealr_closed I.
+  split=> [||a q1 q2 Iq1 Iq2]; first exact: dvdp0.
+    by apply/memI=> [[i /idPn[]]]; rewrite dvdp1 neq_ltn sz_d orbT.
+  apply/memI; exists (maxn (pickle q1).+1 (pickle q2).+1); apply: dvdp_add.
+    by apply: dvdp_mull; apply: dvdp_trans Iq1; apply/dv_d/leq_maxl.
+  by apply: dvdp_trans Iq2; apply/dv_d/leq_maxr.
+pose Iaddkey := GRing.Pred.Add (DefaultPredKey I) I_ideal.
+pose Iidkey := MkIdeal (GRing.Pred.Zmod Iaddkey I_ideal) I_ideal.
+pose E := ComRingType _ (@Quotient.mulqC _ _ _ (KeyedPred Iidkey)).
+pose PtoE : {rmorphism {poly F} -> E} := [rmorphism of \pi_E%qT : {poly F} -> E].
+have PtoEd i: PtoE (d i) = 0.
+  by apply/eqP; rewrite piE Quotient.equivE subr0; apply/memI; exists i.
+pose Einv (z : E) (q := repr z) (dq := d (pickle q).+1) :=
+  let q_unitP := Bezout_eq1_coprimepP q dq in
+  if q_unitP is ReflectT ex_uv then PtoE (sval (sig_eqW ex_uv)).1 else 0.
+have Einv0: Einv 0 = 0.
+  rewrite /Einv; case: Bezout_eq1_coprimepP => // ex_uv.
+  case/negP: (oner_neq0 E); rewrite piE -[_ 1]/(PtoE 1); have [uv <-] := ex_uv.
+  by rewrite rmorphD !rmorphM PtoEd /= reprK !mulr0 addr0.
+have EmulV: GRing.Field.axiom Einv.
+  rewrite /Einv=> z nz_z; case: Bezout_eq1_coprimepP => [ex_uv |]; last first.
+    move/Bezout_eq1_coprimepP; rewrite I'co //.
+    by rewrite piE -{1}[z]reprK -Quotient.idealrBE subr0 in nz_z.
+  apply/eqP; case: sig_eqW => {ex_uv} [uv uv1]; set i := _.+1 in uv1 *.
+  rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE.
+  by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; apply: dvdp_mull.
+pose EringU := [comUnitRingType of UnitRingType _ (FieldUnitMixin EmulV Einv0)].
+have Eunitf := @FieldMixin _ _ EmulV Einv0.
+pose Efield := FieldType (IdomainType EringU (FieldIdomainMixin Eunitf)) Eunitf.
+pose Ecount := CountType Efield (CanCountMixin (@reprK _ _)).
+pose FtoE := [rmorphism of PtoE \o polyC]; pose w : E := PtoE 'X.
+have defPtoE q: (map_poly FtoE q).[w] = PtoE q.
+  by rewrite map_poly_comp horner_map [_.['X]]comp_polyXr.
+exists [countFieldType of Ecount], FtoE, w => [|u].
+  by rewrite /root defPtoE (PtoEd 0%N).
+by exists (repr u); rewrite defPtoE /= reprK.
+Qed.
+
+Lemma countable_algebraic_closure (F : countFieldType) :
+  {K : countClosedFieldType & {FtoK : {rmorphism F -> K} | integralRange FtoK}}.
+Proof.
+pose minXp (R : ringType) (p : {poly R}) := if size p > 1 then p else 'X.
+have minXp_gt1 R p: size (minXp R p) > 1.
+  by rewrite /minXp; case: ifP => // _; rewrite size_polyX.
+have minXpE (R : ringType) (p : {poly R}) : size p > 1 -> minXp R p = p.
+  by rewrite /minXp => ->.
+have ext1 p := countable_field_extension (minXp_gt1 _ p).
+pose ext1fT E p := tag (ext1 E p).
+pose ext1to E p : {rmorphism _ -> ext1fT E p} := tag (tagged (ext1 E p)).
+pose ext1w E p : ext1fT E p := s2val (tagged (tagged (ext1 E p))).
+have ext1root E p: root (map_poly (ext1to E p) (minXp E p)) (ext1w E p).
+  by rewrite /ext1w; case: (tagged (tagged (ext1 E p))).
+have ext1gen E p u: {q | u = (map_poly (ext1to E p) q).[ext1w E p]}.
+  by apply: sig_eqW; rewrite /ext1w; case: (tagged (tagged (ext1 E p))) u.
+pose pExtEnum (E : countFieldType) := nat -> {poly E}.
+pose Ext := {E : countFieldType & pExtEnum E}; pose MkExt : Ext := Tagged _ _.
+pose EtoInc (E : Ext) i := ext1to (tag E) (tagged E i).
+pose incEp E i j :=
+  let v := map_poly (EtoInc E i) (tagged E j) in
+  if decode j is [:: i1; k] then
+    if i1 == i then odflt v (unpickle k) else v
+  else v.
+pose fix E_ i := if i is i1.+1 then MkExt _ (incEp (E_ i1) i1) else MkExt F \0.
+pose E i := tag (E_ i); pose Krep := {i : nat & E i}.
+pose fix toEadd i k : {rmorphism E i -> E (k + i)%N} :=
+  if k is k1.+1 then [rmorphism of EtoInc _ (k1 + i)%N \o toEadd _ _]
+  else [rmorphism of idfun].
+pose toE i j (le_ij : i <= j) :=
+  ecast j {rmorphism E i -> E j} (subnK le_ij) (toEadd i (j - i)%N).
+have toEeq i le_ii: toE i i le_ii =1 id.
+  by rewrite /toE; move: (subnK _); rewrite subnn => ?; rewrite eq_axiomK.
+have toEleS i j leij leiSj z: toE i j.+1 leiSj z = EtoInc _ _ (toE i j leij z).
+  rewrite /toE; move: (j - i)%N {leij leiSj}(subnK _) (subnK _) => k.
+  by case: j /; rewrite (addnK i k.+1) => eq_kk; rewrite [eq_kk]eq_axiomK.
+have toEirr := congr1 ((toE _ _)^~ _) (bool_irrelevance _ _).
+have toEtrans j i k leij lejk leik z:
+  toE i k leik z = toE j k lejk (toE i j leij z).
+- elim: k leik lejk => [|k IHk] leiSk lejSk.
+    by case: j => // in leij lejSk *; rewrite toEeq.
+  have:= lejSk; rewrite {1}leq_eqVlt ltnS => /predU1P[Dk | lejk].
+    by rewrite -Dk in leiSk lejSk *; rewrite toEeq.
+  by have leik := leq_trans leij lejk; rewrite !toEleS -IHk.
+have [leMl leMr] := (leq_maxl, leq_maxr); pose le_max := (leq_max, leqnn, orbT).
+pose pairK (x y : Krep) (m := maxn _ _) :=
+  (toE _ m (leMl _ _) (tagged x), toE _ m (leMr _ _) (tagged y)).
+pose eqKrep x y := prod_curry (@eq_op _) (pairK x y).
+have eqKrefl : reflexive eqKrep by move=> z; apply/eqP; apply: toEirr.
+have eqKsym : symmetric eqKrep.
+  move=> z1 z2; rewrite {1}/eqKrep /= eq_sym; move: (leMl _ _) (leMr _ _).
+  by rewrite maxnC => lez1m lez2m; congr (_ == _); apply: toEirr.
+have eqKtrans : transitive eqKrep.
+  rewrite /eqKrep /= => z2 z1 z3 /eqP eq_z12 /eqP eq_z23.
+  rewrite -(inj_eq (fmorph_inj (toE _ _ (leMr (tag z2) _)))).
+  rewrite -!toEtrans ?le_max // maxnCA maxnA => lez3m lez1m.
+  rewrite {lez1m}(toEtrans (maxn (tag z1) (tag z2))) // {}eq_z12.
+  do [rewrite -toEtrans ?le_max // -maxnA => lez2m] in lez3m *.
+  by rewrite (toEtrans (maxn (tag z2) (tag z3))) // eq_z23 -toEtrans.
+pose K := {eq_quot (EquivRel _  eqKrefl eqKsym eqKtrans)}%qT.
+have cntK : Countable.mixin_of K := CanCountMixin (@reprK _ _).
+pose EtoKrep i (x : E i) : K := \pi%qT (Tagged E x).
+have [EtoK piEtoK]: {EtoK | forall i, EtoKrep i =1 EtoK i} by exists EtoKrep.
+pose FtoK := EtoK 0%N; rewrite {}/EtoKrep in piEtoK.
+have eqEtoK i j x y:
+  toE i _ (leMl i j) x = toE j _ (leMr i j) y -> EtoK i x = EtoK j y.
+- by move/eqP=> eq_xy; rewrite -!piEtoK; apply/eqmodP.
+have toEtoK j i leij x : EtoK j (toE i j leij x) = EtoK i x.
+  by apply: eqEtoK; rewrite -toEtrans.
+have EtoK_0 i: EtoK i 0 = FtoK 0 by apply: eqEtoK; rewrite !rmorph0.
+have EtoK_1 i: EtoK i 1 = FtoK 1 by apply: eqEtoK; rewrite !rmorph1.
+have EtoKeq0 i x: (EtoK i x == FtoK 0) = (x == 0).
+  by rewrite /FtoK -!piEtoK eqmodE /= /eqKrep /= rmorph0 fmorph_eq0.
+have toErepr m i leim x lerm:
+  toE _ m lerm (tagged (repr (EtoK i x))) = toE i m leim x.
+- have: (Tagged E x == repr (EtoK i x) %[mod K])%qT by rewrite reprK piEtoK.
+  rewrite eqmodE /= /eqKrep; case: (repr _) => j y /= in lerm * => /eqP /=.
+  have leijm: maxn i j <= m by rewrite geq_max leim.
+  by move/(congr1 (toE _ _ leijm)); rewrite -!toEtrans.
+pose Kadd (x y : K) := EtoK _ (prod_curry +%R (pairK (repr x) (repr y))).
+pose Kopp (x : K) := EtoK _ (- tagged (repr x)).
+pose Kmul (x y : K) := EtoK _ (prod_curry *%R (pairK (repr x) (repr y))).
+pose Kinv (x : K) := EtoK _ (tagged (repr x))^-1.
+have EtoK_D i: {morph EtoK i : x y / x + y >-> Kadd x y}.
+  move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphD.
+  by rewrite -!toEtrans ?le_max  // => lexm leym; rewrite !toErepr.
+have EtoK_N i: {morph EtoK i : x / - x >-> Kopp x}.
+  by move=> x; apply: eqEtoK; set j := tag _; rewrite !rmorphN toErepr.
+have EtoK_M i: {morph EtoK i : x y / x * y >-> Kmul x y}.
+  move=> x y; apply: eqEtoK; set j := maxn (tag _) _; rewrite !rmorphM.
+  by rewrite -!toEtrans ?le_max  // => lexm leym; rewrite !toErepr.
+have EtoK_V i: {morph EtoK i : x / x^-1 >-> Kinv x}.
+  by move=> x; apply: eqEtoK; set j := tag _; rewrite !fmorphV toErepr.
+case: {toErepr}I in (Kadd) (Kopp) (Kmul) (Kinv) EtoK_D EtoK_N EtoK_M EtoK_V.
+pose inEi i z := {x : E i | z = EtoK i x}; have KtoE z: {i : nat & inEi i z}.
+  by elim/quotW: z => [[i x] /=]; exists i, x; rewrite piEtoK.
+have inEle i j z: i <= j -> inEi i z -> inEi j z.
+  by move=> leij [x ->]; exists (toE i j leij x); rewrite toEtoK.
+have KtoE2 z1 z2: {i : nat & inEi i z1 & inEi i z2}.
+  have [[i1 Ez1] [i2 Ez2]] := (KtoE z1, KtoE z2).
+  by exists (maxn i1 i2); [apply: inEle Ez1 | apply: inEle Ez2].
+have KtoE3 z1 z2 z3: {i : nat & inEi i z1 & inEi i z2 * inEi i z3}%type.
+  have [[i1 Ez1] [i2 Ez2 Ez3]] := (KtoE z1, KtoE2 z2 z3).
+  by exists (maxn i1 i2); [apply: inEle Ez1 | split; apply: inEle (leMr _ _) _].
+have KaddC: commutative Kadd.
+  by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_D addrC.
+have KaddA: associative Kadd.
+  move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w.
+  by rewrite -!EtoK_D addrA.
+have Kadd0: left_id (FtoK 0) Kadd.
+  by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_0 i) -EtoK_D add0r.
+have KaddN: left_inverse (FtoK 0) Kopp Kadd.
+  by move=> u; have [i [x ->]] := KtoE u; rewrite -EtoK_N -EtoK_D addNr EtoK_0.
+pose Kzmod := ZmodType K (ZmodMixin KaddA KaddC Kadd0 KaddN).
+have KmulC: commutative Kmul.
+  by move=> u v; have [i [x ->] [y ->]] := KtoE2 u v; rewrite -!EtoK_M mulrC.
+have KmulA: @associative Kzmod Kmul.
+  move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w.
+  by rewrite -!EtoK_M mulrA.
+have Kmul1: left_id (FtoK 1) Kmul.
+  by move=> u; have [i [x ->]] := KtoE u; rewrite -(EtoK_1 i) -EtoK_M mul1r.
+have KmulD: left_distributive Kmul Kadd.
+  move=> u v w; have [i [x ->] [[y ->] [z ->]]] := KtoE3 u v w.
+  by rewrite -!(EtoK_M, EtoK_D) mulrDl.
+have Kone_nz: FtoK 1 != FtoK 0 by rewrite EtoKeq0 oner_neq0.
+pose KringMixin := ComRingMixin KmulA KmulC Kmul1 KmulD Kone_nz.
+pose Kring := ComRingType (RingType Kzmod KringMixin) KmulC.
+have KmulV: @GRing.Field.axiom Kring Kinv.
+  move=> u; have [i [x ->]] := KtoE u; rewrite EtoKeq0 => nz_x.
+  by rewrite -EtoK_V -[_ * _]EtoK_M mulVf ?EtoK_1.
+have Kinv0: Kinv (FtoK 0) = FtoK 0 by rewrite -EtoK_V invr0.
+pose Kuring := [comUnitRingType of UnitRingType _ (FieldUnitMixin KmulV Kinv0)].
+pose KfieldMixin := @FieldMixin _ _ KmulV Kinv0.
+pose Kidomain := IdomainType Kuring (FieldIdomainMixin KfieldMixin).
+pose Kfield := FieldType Kidomain KfieldMixin.
+have EtoKrmorphism i: rmorphism (EtoK i : E i -> Kfield).
+  by do 2?split=> [x y|]; rewrite ?EtoK_D ?EtoK_N ?EtoK_M ?EtoK_1.
+pose EtoKM := RMorphism (EtoKrmorphism _); have EtoK_E: EtoK _ = EtoKM _ by [].
+have toEtoKp := @eq_map_poly _ Kring _ _(toEtoK _ _ _).
+have Kclosed: GRing.ClosedField.axiom Kfield.
+  move=> n pK n_gt0; pose m0 := \max_(i < n) tag (KtoE (pK i)); pose m := m0.+1.
+  have /fin_all_exists[pE DpE] (i : 'I_n): exists y, EtoK m y = pK i.
+    pose u := KtoE (pK i); have leum0: tag u <= m0 by rewrite (bigmax_sup i).
+    by have [y ->] := tagged u; exists (toE _ _ (leqW leum0) y); rewrite toEtoK.
+  pose p := 'X^n - rVpoly (\row_i pE i); pose j := code [:: m0; pickle p].
+  pose pj := tagged (E_ j) j; pose w : E j.+1 := ext1w (E j) pj.
+  have lemj: m <= j by rewrite (allP (ltn_code _)) ?mem_head.
+  exists (EtoKM j.+1 w); apply/eqP; rewrite -subr_eq0; apply/eqP.
+  transitivity (EtoKM j.+1 (map_poly (toE m j.+1 (leqW lemj)) p).[w]).
+    rewrite -horner_map -map_poly_comp toEtoKp EtoK_E; move/EtoKM: w => w.
+    rewrite rmorphB [_ 'X^n]map_polyXn !hornerE hornerXn; congr (_ - _ : Kring).
+    rewrite (@horner_coef_wide _ n) ?size_map_poly ?size_poly //.
+    by apply: eq_bigr => i _; rewrite coef_map coef_rVpoly valK mxE /= DpE.
+  suffices Dpj: map_poly (toE m j lemj) p = pj.
+    apply/eqP; rewrite EtoKeq0 (eq_map_poly (toEleS _ _ _ _)) map_poly_comp Dpj.
+    rewrite -rootE -[pj]minXpE ?ext1root // -Dpj size_map_poly.
+    by rewrite size_addl ?size_polyXn ltnS ?size_opp ?size_poly.
+  rewrite {w}/pj; elim: {-9}j lemj => // k IHk lemSk.
+  move: lemSk (lemSk); rewrite {1}leq_eqVlt ltnS => /predU1P[<- | lemk] lemSk.
+    rewrite {k IHk lemSk}(eq_map_poly (toEeq m _)) map_poly_id //= /incEp.
+    by rewrite codeK eqxx pickleK.
+  rewrite (eq_map_poly (toEleS _ _ _ _)) map_poly_comp {}IHk //= /incEp codeK.
+  by rewrite -if_neg neq_ltn lemk.
+suffices{Kclosed} algF_K: {FtoK : {rmorphism F -> Kfield} | integralRange FtoK}.
+  pose Kdec := DecFieldType Kfield (closed_field_QEMixin Kclosed).
+  pose KclosedField := ClosedFieldType Kdec Kclosed.
+  by exists [countClosedFieldType of CountType KclosedField cntK].
+exists (EtoKM 0%N) => /= z; have [i [{z}z ->]] := KtoE z.
+suffices{z} /(_ z)[p mon_p]: integralRange (toE 0%N i isT).
+  by rewrite -(fmorph_root (EtoKM i)) -map_poly_comp toEtoKp; exists p.
+rewrite /toE /E; clear - minXp_gt1 ext1root ext1gen.
+move: (i - 0)%N (subnK _) => n; case: i /.
+elim: n => [|n IHn] /= z; first exact: integral_id.
+have{z} [q ->] := ext1gen _ _ z; set pn := tagged (E_ _) _.
+apply: integral_horner.
+  by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph.
+apply: integral_root (ext1root _ _) _.
+  by rewrite map_poly_eq0 -size_poly_gt0 ltnW.
+by apply/integral_poly=> i; rewrite coef_map; apply: integral_rmorph.
+Qed.