(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import bigop ssralg finalg zmodp matrix mxalgebra.
Require Import poly polydiv mxpoly generic_quotient ring_quotient closed_field.
Require Import ssrint rat.

(*****************************************************************************)
(* This file clones part of ssralg hierachy for countable types; it does not *)
(* cover the left module / algebra interfaces, providing only                *)
(*          countZmodType == countable zmodType interface.                   *)
(*          countRingType == countable ringType interface.                   *)
(*       countComRingType == countable comRingType interface.                *)
(*      countUnitRingType == countable unitRingType interface.               *)
(*   countComUnitRingType == countable comUnitRingType interface.            *)
(*       countIdomainType == countable idomainType interface.                *)
(*         countFieldType == countable fieldType interface.                  *)
(*      countDecFieldType == countable decFieldType interface.               *)
(*   countClosedFieldType == countable closedFieldType interface.            *)
(* The interface cloning syntax is extended to these structures              *)
(*   [countZmodType of M] == countZmodType structure for an M that has both  *)
(*                           zmodType and countType structures.              *)
(*                    ... etc                                                *)
(* This file provides constructions for both simple extension and algebraic  *)
(* closure of countable fields.                                              *) 
(*****************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope ring_scope.
Import GRing.Theory CodeSeq.

Module CountRing.

Local Notation mixin_of T := (Countable.mixin_of T).

Section Generic.

(* Implicits *)
Variables (type base_type : Type) (class_of base_of : Type -> Type).
Variable base_sort : base_type -> Type.

(* Explicits *)
Variable Pack : forall T, class_of T -> Type -> type.
Variable Class : forall T, base_of T -> mixin_of T -> class_of T.
Variable base_class : forall bT, base_of (base_sort bT).

Definition gen_pack T :=
  fun bT b & phant_id (base_class bT) b =>
  fun fT c m & phant_id (Countable.class fT) (Countable.Class c m) =>
  Pack (@Class T b m) T.

End Generic.

Implicit Arguments gen_pack [type base_type class_of base_of base_sort].
Local Notation cnt_ c := (@Countable.Class _ c c).
Local Notation do_pack pack T := (pack T _ _ id _ _ _ id).
Import GRing.Theory.

Module Zmodule.

Section ClassDef.

Record class_of M :=
  Class { base : GRing.Zmodule.class_of M; mixin : mixin_of M }.
Local Coercion base : class_of >-> GRing.Zmodule.class_of.
Local Coercion mixin : class_of >-> mixin_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.Zmodule.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.

Definition join_countType := @Countable.Pack zmodType (cnt_ xclass) xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.Zmodule.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Canonical join_countType.
Notation countZmodType := type.
Notation "[ 'countZmodType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'countZmodType'  'of'  T ]") : form_scope.
End Exports.

End Zmodule.
Import Zmodule.Exports.

Module Ring.

Section ClassDef.

Record class_of R := Class { base : GRing.Ring.class_of R; mixin : mixin_of R }.
Definition base2 R (c : class_of R) := Zmodule.Class (base c) (mixin c).
Local Coercion base : class_of >-> GRing.Ring.class_of.
Local Coercion base2 : class_of >-> Zmodule.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.Ring.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass cT.
Definition countZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition join_countType := @Countable.Pack ringType (cnt_ xclass) xT.
Definition join_countZmodType := @Zmodule.Pack ringType xclass xT.

End ClassDef.

Module Import Exports.
Coercion base : class_of >-> GRing.Ring.class_of.
Coercion base2 : class_of >-> Zmodule.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion countZmodType : type >-> Zmodule.type.
Canonical countZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Canonical join_countType.
Canonical join_countZmodType.
Notation countRingType := type.
Notation "[ 'countRingType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'countRingType'  'of'  T ]") : form_scope.
End Exports.

End Ring.
Import Ring.Exports.

Module ComRing.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.ComRing.class_of R; mixin : mixin_of R }.
Definition base2 R (c : class_of R) := Ring.Class (base c) (mixin c).
Local Coercion base : class_of >-> GRing.ComRing.class_of.
Local Coercion base2 : class_of >-> Ring.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.ComRing.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition countZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition countRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition join_countType := @Countable.Pack comRingType (cnt_ xclass) xT.
Definition join_countZmodType := @Zmodule.Pack comRingType xclass xT.
Definition join_countRingType := @Ring.Pack comRingType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.ComRing.class_of.
Coercion base2 : class_of >-> Ring.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion countZmodType : type >-> Zmodule.type.
Canonical countZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion countRingType : type >-> Ring.type.
Canonical countRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Canonical join_countType.
Canonical join_countZmodType.
Canonical join_countRingType.
Notation countComRingType := CountRing.ComRing.type.
Notation "[ 'countComRingType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'countComRingType'  'of'  T ]") : form_scope.
End Exports.

End ComRing.
Import ComRing.Exports.

Module UnitRing.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.UnitRing.class_of R; mixin : mixin_of R }.
Definition base2 R (c : class_of R) := Ring.Class (base c) (mixin c).
Local Coercion base : class_of >-> GRing.UnitRing.class_of.
Local Coercion base2 : class_of >-> Ring.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.UnitRing.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition countZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition countRingType := @Ring.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.

Definition join_countType := @Countable.Pack unitRingType (cnt_ xclass) xT.
Definition join_countZmodType := @Zmodule.Pack unitRingType xclass xT.
Definition join_countRingType := @Ring.Pack unitRingType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.UnitRing.class_of.
Coercion base2 : class_of >-> Ring.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion countZmodType : type >-> Zmodule.type.
Canonical countZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion countRingType : type >-> Ring.type.
Canonical countRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Canonical join_countType.
Canonical join_countZmodType.
Canonical join_countRingType.
Notation countUnitRingType := CountRing.UnitRing.type.
Notation "[ 'countUnitRingType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'countUnitRingType'  'of'  T ]") : form_scope.
End Exports.

End UnitRing.
Import UnitRing.Exports.

Module ComUnitRing.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.ComUnitRing.class_of R; mixin : mixin_of R }.
Definition base2 R (c : class_of R) := ComRing.Class (base c) (mixin c).
Definition base3 R (c : class_of R) := @UnitRing.Class R (base c) (mixin c).
Local Coercion base : class_of >-> GRing.ComUnitRing.class_of.
Local Coercion base2 : class_of >-> ComRing.class_of.
Local Coercion base3 : class_of >-> UnitRing.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.ComUnitRing.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition countZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition countRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition countComRingType := @ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.

Definition join_countType := @Countable.Pack comUnitRingType (cnt_ xclass) xT.
Definition join_countZmodType := @Zmodule.Pack comUnitRingType xclass xT.
Definition join_countRingType := @Ring.Pack comUnitRingType xclass xT.
Definition join_countComRingType := @ComRing.Pack comUnitRingType xclass xT.
Definition join_countUnitRingType := @UnitRing.Pack comUnitRingType xclass xT.
Definition ujoin_countComRingType := @ComRing.Pack unitRingType xclass xT.
Definition cjoin_countUnitRingType := @UnitRing.Pack comRingType xclass xT.
Definition ccjoin_countUnitRingType :=
  @UnitRing.Pack countComRingType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.ComUnitRing.class_of.
Coercion base2 : class_of >-> ComRing.class_of.
Coercion base3 : class_of >-> UnitRing.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion countZmodType : type >-> Zmodule.type.
Canonical countZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion countRingType : type >-> Ring.type.
Canonical countRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion countComRingType : type >-> ComRing.type.
Canonical countComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion countUnitRingType : type >-> UnitRing.type.
Canonical countUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Canonical join_countType.
Canonical join_countZmodType.
Canonical join_countRingType.
Canonical join_countComRingType.
Canonical join_countUnitRingType.
Canonical ujoin_countComRingType.
Canonical cjoin_countUnitRingType.
Canonical ccjoin_countUnitRingType.
Notation countComUnitRingType := CountRing.ComUnitRing.type.
Notation "[ 'countComUnitRingType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'countComUnitRingType'  'of'  T ]") : form_scope.
End Exports.

End ComUnitRing.
Import ComUnitRing.Exports.

Module IntegralDomain.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.IntegralDomain.class_of R; mixin : mixin_of R }.
Definition base2 R (c : class_of R) := ComUnitRing.Class (base c) (mixin c).
Local Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Local Coercion base2 : class_of >-> ComUnitRing.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.IntegralDomain.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition countZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition countRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition countComRingType := @ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.

Definition join_countType := @Countable.Pack idomainType (cnt_ xclass) xT.
Definition join_countZmodType := @Zmodule.Pack idomainType xclass xT.
Definition join_countRingType := @Ring.Pack idomainType xclass xT.
Definition join_countUnitRingType := @UnitRing.Pack idomainType xclass xT.
Definition join_countComRingType := @ComRing.Pack idomainType xclass xT.
Definition join_countComUnitRingType := @ComUnitRing.Pack idomainType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Coercion base2 : class_of >-> ComUnitRing.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion countZmodType : type >-> Zmodule.type.
Canonical countZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion countRingType : type >-> Ring.type.
Canonical countRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion countComRingType : type >-> ComRing.type.
Canonical countComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion countUnitRingType : type >-> UnitRing.type.
Canonical countUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion countComUnitRingType : type >-> ComUnitRing.type.
Canonical countComUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Canonical join_countType.
Canonical join_countZmodType.
Canonical join_countRingType.
Canonical join_countComRingType.
Canonical join_countUnitRingType.
Canonical join_countComUnitRingType.
Notation countIdomainType := CountRing.IntegralDomain.type.
Notation "[ 'countIdomainType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'countIdomainType'  'of'  T ]") : form_scope.
End Exports.

End IntegralDomain.
Import IntegralDomain.Exports.

Module Field.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.Field.class_of R; mixin : mixin_of R }.
Definition base2 R (c : class_of R) := IntegralDomain.Class (base c) (mixin c).
Local Coercion base : class_of >-> GRing.Field.class_of.
Local Coercion base2 : class_of >-> IntegralDomain.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.Field.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition countZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition countRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition countComRingType := @ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition countIdomainType := @IntegralDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.

Definition join_countType := @Countable.Pack fieldType (cnt_ xclass) xT.
Definition join_countZmodType := @Zmodule.Pack fieldType xclass xT.
Definition join_countRingType := @Ring.Pack fieldType xclass xT.
Definition join_countUnitRingType := @UnitRing.Pack fieldType xclass xT.
Definition join_countComRingType := @ComRing.Pack fieldType xclass xT.
Definition join_countComUnitRingType := @ComUnitRing.Pack fieldType xclass xT.
Definition join_countIdomainType := @IntegralDomain.Pack fieldType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.Field.class_of.
Coercion base2 : class_of >-> IntegralDomain.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion countZmodType : type >-> Zmodule.type.
Canonical countZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion countRingType : type >-> Ring.type.
Canonical countRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion countComRingType : type >-> ComRing.type.
Canonical countComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion countUnitRingType : type >-> UnitRing.type.
Canonical countUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion countComUnitRingType : type >-> ComUnitRing.type.
Canonical countComUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion countIdomainType : type >-> IntegralDomain.type.
Canonical countIdomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Canonical join_countType.
Canonical join_countZmodType.
Canonical join_countRingType.
Canonical join_countComRingType.
Canonical join_countUnitRingType.
Canonical join_countComUnitRingType.
Canonical join_countIdomainType.
Notation countFieldType := CountRing.Field.type.
Notation "[ 'countFieldType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'countFieldType'  'of'  T ]") : form_scope.
End Exports.

End Field.
Import Field.Exports.

Module DecidableField.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.DecidableField.class_of R; mixin : mixin_of R }.
Definition base2 R (c : class_of R) := Field.Class (base c) (mixin c).
Local Coercion base : class_of >-> GRing.DecidableField.class_of.
Local Coercion base2 : class_of >-> Field.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.DecidableField.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition countZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition countRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition countComRingType := @ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition countIdomainType := @IntegralDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.
Definition countFieldType := @Field.Pack cT xclass xT.
Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT.

Definition join_countType := @Countable.Pack decFieldType (cnt_ xclass) xT.
Definition join_countZmodType := @Zmodule.Pack decFieldType xclass xT.
Definition join_countRingType := @Ring.Pack decFieldType xclass xT.
Definition join_countUnitRingType := @UnitRing.Pack decFieldType xclass xT.
Definition join_countComRingType := @ComRing.Pack decFieldType xclass xT.
Definition join_countComUnitRingType :=
  @ComUnitRing.Pack decFieldType xclass xT.
Definition join_countIdomainType := @IntegralDomain.Pack decFieldType xclass xT.
Definition join_countFieldType := @Field.Pack decFieldType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.DecidableField.class_of.
Coercion base2 : class_of >-> Field.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion countZmodType : type >-> Zmodule.type.
Canonical countZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion countRingType : type >-> Ring.type.
Canonical countRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion countComRingType : type >-> ComRing.type.
Canonical countComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion countUnitRingType : type >-> UnitRing.type.
Canonical countUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion countComUnitRingType : type >-> ComUnitRing.type.
Canonical countComUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion countIdomainType : type >-> IntegralDomain.type.
Canonical countIdomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion countFieldType : type >-> Field.type.
Canonical countFieldType.
Coercion decFieldType : type >-> GRing.DecidableField.type.
Canonical decFieldType.
Canonical join_countType.
Canonical join_countZmodType.
Canonical join_countRingType.
Canonical join_countComRingType.
Canonical join_countUnitRingType.
Canonical join_countComUnitRingType.
Canonical join_countIdomainType.
Canonical join_countFieldType.
Notation countDecFieldType := CountRing.DecidableField.type.
Notation "[ 'countDecFieldType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'countDecFieldType'  'of'  T ]") : form_scope.
End Exports.

End DecidableField.
Import DecidableField.Exports.

Module ClosedField.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.ClosedField.class_of R; mixin : mixin_of R }.
Definition base2 R (c : class_of R) := DecidableField.Class (base c) (mixin c).
Local Coercion base : class_of >-> GRing.ClosedField.class_of.
Local Coercion base2 : class_of >-> DecidableField.class_of.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Definition pack := gen_pack Pack Class GRing.ClosedField.class.
Variable cT : type.
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition countType := @Countable.Pack cT (cnt_ xclass) xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition countZmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition countRingType := @Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition countComRingType := @ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition countUnitRingType := @UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition countIdomainType := @IntegralDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.
Definition countFieldType := @Field.Pack cT xclass xT.
Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT.
Definition countDecFieldType := @DecidableField.Pack cT xclass xT.
Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT.

Definition join_countType := @Countable.Pack closedFieldType (cnt_ xclass) xT.
Definition join_countZmodType := @Zmodule.Pack closedFieldType xclass xT.
Definition join_countRingType := @Ring.Pack closedFieldType xclass xT.
Definition join_countUnitRingType := @UnitRing.Pack closedFieldType xclass xT.
Definition join_countComRingType := @ComRing.Pack closedFieldType xclass xT.
Definition join_countComUnitRingType :=
  @ComUnitRing.Pack closedFieldType xclass xT.
Definition join_countIdomainType :=
  @IntegralDomain.Pack closedFieldType xclass xT.
Definition join_countFieldType := @Field.Pack closedFieldType xclass xT.
Definition join_countDecFieldType :=
  @DecidableField.Pack closedFieldType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.ClosedField.class_of.
Coercion base2 : class_of >-> DecidableField.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion countZmodType : type >-> Zmodule.type.
Canonical countZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion countRingType : type >-> Ring.type.
Canonical countRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion countComRingType : type >-> ComRing.type.
Canonical countComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion countUnitRingType : type >-> UnitRing.type.
Canonical countUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion countComUnitRingType : type >-> ComUnitRing.type.
Canonical countComUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion countFieldType : type >-> Field.type.
Canonical countFieldType.
Coercion decFieldType : type >-> GRing.DecidableField.type.
Canonical decFieldType.
Coercion countDecFieldType : type >-> DecidableField.type.
Canonical countDecFieldType.
Coercion closedFieldType : type >-> GRing.ClosedField.type.
Canonical closedFieldType.
Canonical join_countType.
Canonical join_countZmodType.
Canonical join_countRingType.
Canonical join_countComRingType.
Canonical join_countUnitRingType.
Canonical join_countComUnitRingType.
Canonical join_countIdomainType.
Canonical join_countFieldType.
Canonical join_countDecFieldType.
Notation countClosedFieldType := CountRing.ClosedField.type.
Notation "[ 'countClosedFieldType' 'of' T ]" := (do_pack pack T)
  (at level 0, format "[ 'countClosedFieldType'  'of'  T ]") : form_scope.
End Exports.

End ClosedField.
Import ClosedField.Exports.

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.

Require Import poly polydiv generic_quotient ring_quotient.
Require Import mxpoly polyXY.
Import GRing.Theory.
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; exact: 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.