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

9 files changed, 918 insertions, 11 deletions

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/algebra/countalg.v b/mathcomp/algebra/countalg.v
new file mode 100644
index 0000000..21000e4
--- /dev/null
+++ b/mathcomp/algebra/countalg.v
@@ -0,0 +1,797 @@
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
+(* Distributed under the terms of CeCILL-B.                                  *)
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
+From mathcomp
+Require Import bigop ssralg generic_quotient ring_quotient.
+
+(*****************************************************************************)
+(* 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.
+
+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.
\ 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].