Library ssralg

  The algebraic part of the Algebraic Hierarchy, as described in          
          ``Packaging mathematical structures'', TPHOLs09, by              
   Francois Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau    



This file defines for each Structure (Zmodule, Ring, etc ...) its type, its packers and its canonical properties :

Zmodule

zmodType == type for Zmodule structure ZmodMixin == builds the mixin containing the definition of a Zmodule ZmodType R M == packs the mixin M to build a Zmodule of type zmodType. (The underlying type R should have a choiceType canonical structure) 0 == the additive identity element of a Zmodule x + y == the addition operation of a Zmodule - x == the opposite operation of a Zmodule x - y == the substraction operation of a Zmodule := x + - y x +* n , x -* n == the generic multiplication by a nat \sum_<range> e == iterated sum for a Zmodule (cf bigops.v) e`_i == nth 0 e i, when e : seq M and M is a zmodType ... and a many classical Lemmas on these Zmodule laws

Ring

ringType == type for ring structure RingMixin == builds the mixin containing the definitions of a ring (the underlying type should have a zmodType structure) RingType R M == packs the ring mixin M to build a ring on type R RevRingType T == repacks T to build the ring where the multiplicative law is reversed ( x *' y = y * x ) 1 == the multiplicative identity element of a Ring n%:R == the ring image of a nat n (e.g., 1%:R := 1%R) x * y == the multiplication operation of a ring \prod_<range> e == iterated product for a ring (cf bigops.v) x ^+ y == the exponentiation operation of a ring GRing.comm x y <=> x and y commute, i.e., x * y = y * x [char R] == the characteristic of R, i.e., the set of prime numbers p such that p%:R = 0 in R. The set [char p] has a most one element, and is represented as a pred_nat collective predicate (see prime.v); thus the statement p \in [char R] can be read as ``R has characteristic p'', while [char R] =i pred0 means ``R has characteristic 0'' when R is a field. Frobenius_aut chRp == the Frobenius automorphism mapping x : R to x ^+ p, where chRp : p \in [char R] is a proof that R has indeed (non-zero) characteristic p.

Commutative Ring

comRingType == type for commutative ring structure ComRingType R mulC == packs mulC to build a commutative ring. (The underlying type R should have a ring canonical structure) ComRingMixin == builds the mixin containing the definitions of a *non commutative* ring, using the commutativity to decrease the number of axioms.

Unit Ring

unitRingType == type for unit ring structure UnitRingMixin == builds the mixin containing the definitions of a unit ring. (The underlying type should have a ring canonical structure) UnitRingType R M == packs the unit ring mixin M to build a unit ring. WARNING: while it is possible to omit R for most of the xxxType functions, R MUST be explicitly given when UnitRingType is used with a mixin produced by ComUnitRingMixin, otherwise the resulting structure will have the WRONG sort and will not be used by type inference. GRing.unit x == x is a unit (i.e., has an inverse) x^-1 == the inversion operation element of a unit ring (returns x if is x is not an unit) x / y := x * y^-1 x ^- n := (x ^+ n)^-1

Commutative Unit Ring

comUnitRingType == type for unit ring structure ComUnitRingMixin == builds the mixin containing the definitions of a *non commutative unit ring*, but using the commutative property. The underlying type should have a commutative ring canonical structure. WARNING: ALWAYS give an explicit type argument to UnitRingType along with a mixin produced by ComUnitRingMixin (see above).

Integral Domain (integral, commutative, unit ring)

idomainType == type for integral domain structure IdomainType R M == packs the idomain mixin M to build a integral domain. (The underlying type R should have a commutative unit ring canonical structure)

Field

fieldType == type for field structure FieldUnitMixin == builds a *non commutative unit ring* mixin, using some field properties. (The underlying type should have a *commutative ring* canonical structure) FieldMixin == builds the field mixin. (The underlying type should have a *commutative ring* canonical structure) FieldIdomainMixin == builds an *idomain* mixin, using a field mixin FieldType R M == packs the field mixin M to build a field (The underlying type R should have a integral domain canonical structure)

Decidable Field

decFieldType == type for decidable field structure DecFieldMixin == builds the mixin containing the definitions of a decidable Field. (The underlying type should have a unit ring canonical structure) DecFieldType R M == packs the decidable field mixin M to build a decidable field. (The underlying type R should have a field canonical structure) GRing.term R == the type of formal expressions in a unit ring R with formal variables 'X_k, k : nat, and manifest constants x%:T, x : R. The notation of all the ring operations is redefined for terms, in scope %T. GRing.formula R == the type of first order formulas over R; the %T scope binds the logical connectives /\, \/, ~, ==>, ==, and != to formulae; GRing.True/False and GRing.Bool b denote constant formulae, and quantifiers are written 'forall/'exists 'X_k, f GRing.Unit x tests for ring units, and the the construct Pick p_f t_f e_f can be used to emulate the pick function defined in fintype.v. GRing.eval e t == the value of term t with valuation e : seq R (e maps 'X_i to e`_i) GRing.same_env e1 e2 <=> environments e1 and e2 are extensionally equal GRing.qf_eval e f == the value (in bool) of a quantifier-free f. GRing.qf_form f == f is quantifier-free. GRing.holds e f == the intuitionistic CiC interpretation of the formula f holds with valuation e GRing.sat e f == valuation e satisfies f (only in a decField) GRing.sol n f == a sequence e of size n such that e satisfies f, if one exists, or [::] if there is no such e

Closed Field

closedFieldType == type for closed field structure ClosedFieldType R M == packs the closed field mixin M to build a closed field. (The underlying type R should have a decidable field canonical structure.)

Morphism

GRing.morphism f <=> f is a ring morphism: f commutes with 0, +, -, *, 1, and with ^-1 and / in integral domains. x^f == the image of x under some morphism. This notation is only reserved (not defined) here; it is bound locally in sections where some morphism is used heavily (e.g., the container morphism in the parametricity sections of poly and matrix, or the Frobenius section here).

Lmodule

lmodType R == type for Lmodule structure over the ring R LmodMixin R == builds the mixin containing the definition of a Lmodule over the ring R LmodType R T M == packs the mixin M to build a Lmodule of type lmodType R. (The underlying type T should have a zmodType canonical structure) a *: x == the external operation of a Lmodule

The Lemmas about theses structures are all contained in GRing.Theory. Notations are defined in scope ring_scope (delimiter %R), except term and formula notations, which are in term_scope (delimiter %T).

NB: The module GRing should not be imported, only the main module and GRing.Theory should be.

Import Prenex Implicits.

Abstract algebra framework for ssreflect.                          
 We define a number of structures that ``package'' common algebraic 
 properties of operations. These extend the combinatorial classes   
 with notation and theory for classical algebraic structures.       

Reserved Notation "+%R" (at level 0).
Reserved Notation "-%R" (at level 0).
Reserved Notation "*%R" (at level 0).
Reserved Notation "n %:R" (at level 2, left associativity, format "n %:R").
Reserved Notation "[ 'char' F ]" (at level 0, format "[ 'char' F ]").

Reserved Notation "x %:T" (at level 2, left associativity, format "x %:T").
Reserved Notation "''X_' i" (at level 8, i at level 2, format "''X_' i").
Patch for recurring Coq parser bug: Coq seg faults when a level 200 
 notation is used as a pattern.                                      
Reserved Notation "''exists' ''X_' i , f"
  (at level 199, i at level 2, right associativity,
   format "'[hv' ''exists' ''X_' i , '/ ' f ']'").
Reserved Notation "''forall' ''X_' i , f"
  (at level 199, i at level 2, right associativity,
   format "'[hv' ''forall' ''X_' i , '/ ' f ']'").

Reserved Notation "x ^f" (at level 2, left associativity, format "x ^f").

Delimit Scope ring_scope with R.
Delimit Scope term_scope with T.
Local Open Scope ring_scope.

Module GRing.

Import Monoid.Theory.

Module Zmodule.

Record mixin_of (M : Type) : Type := Mixin {
  zero : M;
  opp : M -> M;
  add : M -> M -> M;
  _ : associative add;
  _ : commutative add;
  _ : left_id zero add;
  _ : left_inverse zero opp add
}.

Record class_of (M : Type) : Type :=
  Class { base :> Choice.class_of M; ext :> mixin_of M }.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T m :=
  fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.

End Zmodule.

Canonical Structure Zmodule.eqType.
Canonical Structure Zmodule.choiceType.

Definition zero M := Zmodule.zero (Zmodule.class M).
Definition opp M := Zmodule.opp (Zmodule.class M).
Definition add M := Zmodule.add (Zmodule.class M).

Local Notation "0" := (zero _) : ring_scope.
Local Notation "-%R" := (@opp _) : ring_scope.
Local Notation "- x" := (opp x) : ring_scope.
Local Notation "+%R" := (@add _) : ring_scope.
Local Notation "x + y" := (add x y) : ring_scope.
Local Notation "x - y" := (x + - y) : ring_scope.

Definition natmul M x n := nosimpl iterop _ n +%R x (zero M).

Local Notation "x *+ n" := (natmul x n) : ring_scope.
Local Notation "x *- n" := ((- x) *+ n) : ring_scope.

Local Notation "\sum_ ( i <- r | P ) F" := (\big[+%R/0]_(i <- r | P) F).
Local Notation "\sum_ ( m <= i < n ) F" := (\big[+%R/0]_(m <= i < n) F).
Local Notation "\sum_ ( i < n ) F" := (\big[+%R/0]_(i < n) F).
Local Notation "\sum_ ( i \in A ) F" := (\big[+%R/0]_(i \in A) F).

Local Notation "s `_ i" := (nth 0 s i) : ring_scope.

Section ZmoduleTheory.

Variable M : Zmodule.type.
Implicit Types x y : M.

Lemma addrA : @associative M +%R.

Lemma addrC : @commutative M M +%R.

Lemma add0r : @left_id M M 0 +%R.

Lemma addNr : @left_inverse M M M 0 -%R +%R.

Lemma addr0 : @right_id M M 0 +%R.
Lemma addrN : @right_inverse M M M 0 -%R +%R.
Definition subrr := addrN.

Canonical Structure add_monoid := Monoid.Law addrA add0r addr0.
Canonical Structure add_comoid := Monoid.ComLaw addrC.

Lemma addrCA : @left_commutative M M +%R.

Lemma addrAC : @right_commutative M M +%R.

Lemma addKr : @left_loop M M -%R +%R.
Lemma addNKr : @rev_left_loop M M -%R +%R.
Lemma addrK : @right_loop M M -%R +%R.
Lemma addrNK : @rev_right_loop M M -%R +%R.
Definition subrK := addrNK.
Lemma addrI : @right_injective M M M +%R.
Lemma addIr : @left_injective M M M +%R.
Lemma opprK : @involutive M -%R.
Lemma oppr0 : -0 = 0 :> M.
Lemma oppr_eq0 : forall x, (- x == 0) = (x == 0).

Lemma subr0 : forall x, x - 0 = x.

Lemma sub0r : forall x, 0 - x = - x.

Lemma oppr_add : {morph -%R: x y / x + y : M}.

Lemma oppr_sub : forall x y, - (x - y) = y - x.

Lemma subr_eq : forall x y z, (x - z == y) = (x == y + z).

Lemma subr_eq0 : forall x y, (x - y == 0) = (x == y).

Lemma mulr0n : forall x, x *+ 0 = 0.

Lemma mulr1n : forall x, x *+ 1 = x.

Lemma mulrS : forall x n, x *+ n.+1 = x + x *+ n.

Lemma mulrSr : forall x n, x *+ n.+1 = x *+ n + x.

Lemma mulrb : forall x (b : bool), x *+ b = (if b then x else 0).

Lemma mul0rn : forall n, 0 *+ n = 0 :> M.

Lemma oppr_muln : forall x n, - (x *+ n) = x *- n :> M.

Lemma mulrn_addl : forall n, {morph (fun x => x *+ n) : x y / x + y}.

Lemma mulrn_addr : forall x m n, x *+ (m + n) = x *+ m + x *+ n.

Lemma mulrnA : forall x m n, x *+ (m * n) = x *+ m *+ n.

Lemma mulrnAC : forall x m n, x *+ m *+ n = x *+ n *+ m.

Lemma sumr_opp : forall I r P (F : I -> M),
  (\sum_(i <- r | P i) - F i = - (\sum_(i <- r | P i) F i)).

Lemma sumr_sub : forall I r (P : pred I) (F1 F2 : I -> M),
  \sum_(i <- r | P i) (F1 i - F2 i)
     = \sum_(i <- r | P i) F1 i - \sum_(i <- r | P i) F2 i.

Lemma sumr_muln : forall I r P (F : I -> M) n,
  \sum_(i <- r | P i) F i *+ n = (\sum_(i <- r | P i) F i) *+ n.

Lemma sumr_muln_r : forall x I r P (F : I -> nat),
  \sum_(i <- r | P i) x *+ F i = x *+ (\sum_(i <- r | P i) F i).

Lemma sumr_const : forall (I : finType) (A : pred I) (x : M),
  \sum_(i \in A) x = x *+ #|A|.

End ZmoduleTheory.

Module Ring.

Record mixin_of (R : Zmodule.type) : Type := Mixin {
  one : R;
  mul : R -> R -> R;
  _ : associative mul;
  _ : left_id one mul;
  _ : right_id one mul;
  _ : left_distributive mul +%R;
  _ : right_distributive mul +%R;
  _ : one != 0
}.

Definition EtaMixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 :=
  let _ := @Mixin R one mul mulA mul1x mulx1 mul_addl mul_addr nz1 in
  @Mixin (Zmodule.Pack (Zmodule.class R) R) _ _
     mulA mul1x mulx1 mul_addl mul_addr nz1.

Record class_of (R : Type) : Type := Class {
  base :> Zmodule.class_of R;
  ext :> mixin_of (Zmodule.Pack base R)
}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T b0 (m0 : mixin_of (@Zmodule.Pack T b0 T)) :=
  fun bT b & phant_id (Zmodule.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.

End Ring.

Canonical Structure Ring.eqType.
Canonical Structure Ring.choiceType.
Canonical Structure Ring.zmodType.

Definition one (R : Ring.type) : R := Ring.one (Ring.class R).
Definition mul (R : Ring.type) : R -> R -> R := Ring.mul (Ring.class R).
Definition exp R x n := nosimpl iterop _ n (@mul R) x (one R).

Local Notation "1" := (one _).
Local Notation "- 1" := (- (1)).
Local Notation "n %:R" := (1 *+ n).
Local Notation "*%R" := (@mul _).
Local Notation "x * y" := (mul x y).
Local Notation "x ^+ n" := (exp x n).

Local Notation "\prod_ ( i <- r | P ) F" := (\big[*%R/1]_(i <- r | P) F).
Local Notation "\prod_ ( i \in A ) F" := (\big[*%R/1]_(i \in A) F).

The ``field'' characteristic; the definition, and many of the theorems,   
 has to apply to rings as well; indeed, we need the Frobenius automorphism 
 results for a non commutative ring in the proof of Gorenstein 2.6.3.      
Definition char (R : Ring.type) of phant R : nat_pred :=
  [pred p | prime p && (p%:R == 0 :> R)].

Local Notation "[ 'char' R ]" := (char (Phant R)) : ring_scope.

Section RingTheory.

Variable R : Ring.type.
Implicit Types x y : R.

Lemma mulrA : @associative R *%R.

Lemma mul1r : @left_id R R 1 *%R.

Lemma mulr1 : @right_id R R 1 *%R.

Lemma mulr_addl : @left_distributive R R *%R +%R.
Lemma mulr_addr : @right_distributive R R *%R +%R.
Lemma nonzero1r : 1 != 0 :> R.

Lemma oner_eq0 : (1 == 0 :> R) = false.

Lemma mul0r : @left_zero R R 0 *%R.
Lemma mulr0 : @right_zero R R 0 *%R.
Lemma mulrN : forall x y, x * (- y) = - (x * y).
Lemma mulNr : forall x y, (- x) * y = - (x * y).
Lemma mulrNN : forall x y, (- x) * (- y) = x * y.
Lemma mulN1r : forall x, -1 * x = - x.
Lemma mulrN1 : forall x, x * -1 = - x.

Canonical Structure mul_monoid := Monoid.Law mulrA mul1r mulr1.
Canonical Structure muloid := Monoid.MulLaw mul0r mulr0.
Canonical Structure addoid := Monoid.AddLaw mulr_addl mulr_addr.

Lemma mulr_subl : forall x y z, (y - z) * x = y * x - z * x.

Lemma mulr_subr : forall x y z, x * (y - z) = x * y - x * z.

Lemma mulrnAl : forall x y n, (x *+ n) * y = (x * y) *+ n.

Lemma mulrnAr : forall x y n, x * (y *+ n) = (x * y) *+ n.

Lemma mulr_natl : forall x n, n%:R * x = x *+ n.

Lemma mulr_natr : forall x n, x * n%:R = x *+ n.

Lemma natr_add : forall m n, (m + n)%:R = m%:R + n%:R :> R.

Lemma natr_mul : forall m n, (m * n)%:R = m%:R * n%:R :> R.

Lemma expr0 : forall x, x ^+ 0 = 1.

Lemma expr1 : forall x, x ^+ 1 = x.

Lemma exprS : forall x n, x ^+ n.+1 = x * x ^+ n.

Lemma exp1rn : forall n, 1 ^+ n = 1 :> R.

Lemma exprn_addr : forall x m n, x ^+ (m + n) = x ^+ m * x ^+ n.

Lemma exprSr : forall x n, x ^+ n.+1 = x ^+ n * x.

Definition commDef x y := x * y = y * x.
Notation comm := commDef.

Lemma commr_sym : forall x y, comm x y -> comm y x.

Lemma commr_refl : forall x, comm x x.

Lemma commr0 : forall x, comm x 0.

Lemma commr1 : forall x, comm x 1.

Lemma commr_opp : forall x y, comm x y -> comm x (- y).

Lemma commrN1 : forall x, comm x (-1).

Lemma commr_add : forall x y z,
  comm x y -> comm x z -> comm x (y + z).

Lemma commr_muln : forall x y n, comm x y -> comm x (y *+ n).

Lemma commr_mul : forall x y z,
  comm x y -> comm x z -> comm x (y * z).

Lemma commr_nat : forall x n, comm x n%:R.

Lemma commr_exp : forall x y n, comm x y -> comm x (y ^+ n).

Lemma commr_exp_mull : forall x y n,
  comm x y -> (x * y) ^+ n = x ^+ n * y ^+ n.

Lemma commr_sign : forall x n, comm x ((-1) ^+ n).

Lemma exprn_mulnl : forall x m n, (x *+ m) ^+ n = x ^+ n *+ (m ^ n) :> R.

Lemma exprn_mulr : forall x m n, x ^+ (m * n) = x ^+ m ^+ n.

Lemma natr_exp : forall n k, (n ^ k)%:R = n%:R ^+ k :> R.

Lemma signr_odd : forall n, (-1) ^+ (odd n) = (-1) ^+ n :> R.

Lemma signr_eq0 : forall n, ((-1) ^+ n == 0 :> R) = false.

Lemma signr_addb : forall b1 b2,
  (-1) ^+ (b1 (+) b2) = (-1) ^+ b1 * (-1) ^+ b2 :> R.

Lemma exprN : forall x n, (- x) ^+ n = (-1) ^+ n * x ^+ n :> R.

Lemma prodr_const : forall (I : finType) (A : pred I) (x : R),
  \prod_(i \in A) x = x ^+ #|A|.

Lemma prodr_exp_r : forall x I r P (F : I -> nat),
  \prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i).

Lemma prodr_opp : forall (I : finType) (A : pred I) (F : I -> R),
  \prod_(i \in A) - F i = (- 1) ^+ #|A| * \prod_(i \in A) F i.

Lemma exprn_addl_comm : forall x y n, comm x y ->
  (x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) * y ^+ i) *+ 'C(n, i).

Lemma exprn_subl_comm : forall x y n, comm x y ->
  (x - y) ^+ n =
      \sum_(i < n.+1) ((-1) ^+ i * x ^+ (n - i) * y ^+ i) *+ 'C(n, i).

Lemma subr_expn_comm : forall x y n, comm x y ->
  x ^+ n - y ^+ n = (x - y) * (\sum_(i < n) x ^+ (n.-1 - i) * y ^+ i).

Lemma subr_expn_1 : forall x n, x ^+ n - 1 = (x - 1) * (\sum_(i < n) x ^+ i).

Definition Frobenius_aut p of p \in [char R] := fun x => x ^+ p.

Section Frobenius.

Variable p : nat.
Hypothesis charFp : p \in [char R].

Lemma charf0 : p%:R = 0 :> R.

Lemma charf_prime : prime p.

Hint Resolve charf_prime.

Lemma dvdn_charf : forall n, (p %| n)%N = (n%:R == 0 :> R).

Lemma charf_eq : [char R] =i (p : nat_pred).

Lemma bin_lt_charf_0 : forall k, 0 < k < p -> 'C(p, k)%:R = 0 :> R.

Local Notation "x ^f" := (Frobenius_aut charFp x).

Lemma Frobenius_autE : forall x, x^f = x ^+ p.

Local Notation fE := Frobenius_autE.

Lemma Frobenius_aut_0 : 0^f = 0.

Lemma Frobenius_aut_1 : 1^f = 1.

Lemma Frobenius_aut_add_comm : forall x y, comm x y -> (x + y)^f = x^f + y^f.

Lemma Frobenius_aut_muln : forall x n, (x *+ n)^f = x^f *+ n.

Lemma Frobenius_aut_nat : forall n, (n%:R)^f = n%:R.

Lemma Frobenius_aut_mul_comm : forall x y, comm x y -> (x * y)^f = x^f * y^f.

Lemma Frobenius_aut_exp : forall x n, (x ^+ n)^f = x^f ^+ n.

Lemma Frobenius_aut_opp : forall x, (- x)^f = - x^f.

Lemma Frobenius_aut_sub_comm : forall x y, comm x y -> (x - y)^f = x^f - y^f.

End Frobenius.

Definition RevRingMixin :=
  let mul' x y := y * x in
  let mulrA' x y z := esym (mulrA z y x) in
  let mulr_addl' x y z := mulr_addr z x y in
  let mulr_addr' x y z := mulr_addl y z x in
  @Ring.Mixin R 1 mul' mulrA' mulr1 mul1r mulr_addl' mulr_addr' nonzero1r.

Definition RevRingType := Ring.Pack (Ring.Class RevRingMixin) R.

End RingTheory.

Notation comm := (@commDef _).

Notation rev :=
  (let R := _ in fun (x : Ring.sort R) => x : Ring.sort (RevRingType R)).

Definition morphism (aR rR : Ring.type) (f : aR -> rR) :=
  [/\ {morph f : x y / x - y}, {morph f : x y / x * y} & f 1 = 1].

Section RingMorphTheory.

Variables aR' aR rR : Ring.type.
Variables (f : aR -> rR) (g : aR' -> aR).
Hypotheses (fM : morphism f) (gM : morphism g).

Lemma ringM_sub : {morph f : x y / x - y}.

Lemma ringM_0 : f 0 = 0.

Lemma ringM_1 : f 1 = 1.

Lemma ringM_opp : {morph f : x / - x}.

Lemma ringM_add : {morph f : x y / x + y}.

Definition ringM_sum := big_morph f ringM_add ringM_0.

Lemma ringM_mul : {morph f : x y / x * y}.

Definition ringM_prod := big_morph f ringM_mul ringM_1.

Lemma ringM_natmul : forall n, {morph f : x / x *+ n}.

Lemma ringM_nat : forall n, f n%:R = n %:R.

Lemma ringM_exp : forall n, {morph f : x / x ^+ n}.

Lemma ringM_sign : forall k, f ((- 1) ^+ k) = (- 1) ^+ k.

Lemma ringM_char : forall p, p \in [char aR] -> p \in [char rR].

Lemma comp_ringM : morphism (f \o g).

Lemma ringM_isom :
  bijective f -> exists f', [/\ cancel f f', cancel f' f & morphism f'].

End RingMorphTheory.

Module ComRing.

Record class_of (R : Type) : Type :=
  Class {base :> Ring.class_of R; _ : commutative (Ring.mul base)}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T mul0 (m0 : @commutative T T mul0) :=
  fun bT b & phant_id (Ring.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Definition RingMixin R one mul mulA mulC mul1x mul_addl :=
  let mulx1 := Monoid.mulC_id mulC mul1x in
  let mul_addr := Monoid.mulC_dist mulC mul_addl in
  @Ring.EtaMixin R one mul mulA mul1x mulx1 mul_addl mul_addr.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.

End ComRing.

Canonical Structure ComRing.eqType.
Canonical Structure ComRing.choiceType.
Canonical Structure ComRing.zmodType.
Canonical Structure ComRing.ringType.

Section ComRingTheory.

Variable R : ComRing.type.
Implicit Types x y : R.

Lemma mulrC : @commutative R R *%R.

Canonical Structure mul_comoid := Monoid.ComLaw mulrC.
Lemma mulrCA : @left_commutative R R *%R.

Lemma mulrAC : @right_commutative R R *%R.

Lemma exprn_mull : forall n, {morph (fun x => x ^+ n) : x y / x * y}.

Lemma prodr_exp : forall n I r (P : pred I) (F : I -> R),
  \prod_(i <- r | P i) F i ^+ n = (\prod_(i <- r | P i) F i) ^+ n.

Lemma exprn_addl : forall x y n,
  (x + y) ^+ n = \sum_(i < n.+1) (x ^+ (n - i) * y ^+ i) *+ 'C(n, i).

Lemma exprn_subl : forall x y n,
  (x - y) ^+ n =
     \sum_(i < n.+1) ((-1) ^+ i * x ^+ (n - i) * y ^+ i) *+ 'C(n, i).

Lemma subr_expn : forall x y n,
  x ^+ n - y ^+ n = (x - y) * (\sum_(i < n) x ^+ (n.-1 - i) * y ^+ i).

Lemma ringM_comm : forall (rR : Ring.type) (f : R -> rR),
  morphism f -> forall x y, comm (f x) (f y).

Lemma Frobenius_aut_RM : forall p (charRp : p \in [char R]),
  morphism (Frobenius_aut charRp).

End ComRingTheory.

Module UnitRing.

Record mixin_of (R : Ring.type) : Type := Mixin {
  unit : pred R;
  inv : R -> R;
  _ : {in unit, left_inverse 1 inv *%R};
  _ : {in unit, right_inverse 1 inv *%R};
  _ : forall x y, y * x = 1 /\ x * y = 1 -> unit x;
  _ : {in predC unit, inv =1 id}
}.

Definition EtaMixin R unit inv mulVr mulrV unitP inv_out :=
  let _ := @Mixin R unit inv mulVr mulrV unitP inv_out in
  @Mixin (Ring.Pack (Ring.class R) R) unit inv mulVr mulrV unitP inv_out.

Record class_of (R : Type) : Type := Class {
  base :> Ring.class_of R;
  mixin :> mixin_of (Ring.Pack base R)
}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T b0 (m0 : mixin_of (@Ring.Pack T b0 T)) :=
  fun bT b & phant_id (Ring.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.

End UnitRing.

Canonical Structure UnitRing.eqType.
Canonical Structure UnitRing.zmodType.
Canonical Structure UnitRing.ringType.

Definition unitDef (R : UnitRing.type) : pred R :=
  UnitRing.unit (UnitRing.class R).
Notation unit := (@unitDef _).
Definition inv (R : UnitRing.type) : R -> R := UnitRing.inv (UnitRing.class R).

Notation Local "x ^-1" := (inv x).
Notation Local "x / y" := (x * y^-1).
Notation Local "x ^- n" := ((x ^+ n)^-1).

Section UnitRingTheory.

Variable R : UnitRing.type.
Implicit Types x y : R.

Lemma divrr : forall x, unit x -> x / x = 1.
Definition mulrV := divrr.

Lemma mulVr : forall x, unit x -> x^-1 * x = 1.

Lemma invr_out : forall x, ~~ unit x -> x^-1 = x.

Lemma unitrP : forall x, reflect (exists y, y * x = 1 /\ x * y = 1) (unit x).

Lemma mulKr : forall x, unit x -> cancel (mul x) (mul x^-1).

Lemma mulVKr : forall x, unit x -> cancel (mul x^-1) (mul x).

Lemma mulrK : forall x, unit x -> cancel ( *%R^~ x) ( *%R^~ x^-1).

Lemma mulrVK : forall x, unit x -> cancel ( *%R^~ x^-1) ( *%R^~ x).
Definition divrK := mulrVK.

Lemma mulrI : forall x, unit x -> injective (mul x).

Lemma mulIr : forall x, unit x -> injective ( *%R^~ x).

Lemma commr_inv : forall x, comm x x^-1.

Lemma unitrE : forall x, unit x = (x / x == 1).

Lemma invrK : involutive (@inv R).

Lemma invr_inj : injective (@inv R).

Lemma unitr_inv : forall x, unit x^-1 = unit x.

Lemma unitr1 : unit (1 : R).

Lemma invr1 : 1^-1 = 1 :> R.

Lemma unitr0 : unit (0 : R) = false.

Lemma invr0 : 0^-1 = 0 :> R.

Lemma unitr_opp : forall x, unit (- x) = unit x.

Lemma invrN : forall x, (- x)^-1 = - x^-1.

Lemma unitr_mull : forall x y, unit y -> unit (x * y) = unit x.

Lemma unitr_mulr : forall x y, unit x -> unit (x * y) = unit y.

Lemma invr_mul : forall x y, unit x -> unit y -> (x * y)^-1 = y^-1 * x^-1.

Lemma commr_unit_mul : forall x y, comm x y -> unit (x * y) = unit x && unit y.

Lemma unitr_exp : forall x n, unit x -> unit (x ^+ n).

Lemma unitr_pexp : forall x n, n > 0 -> unit (x ^+ n) = unit x.

Lemma expr_inv : forall x n, x^-1 ^+ n = x ^- n.

Lemma invr_neq0 : forall x, x != 0 -> x^-1 != 0.

Lemma invr_eq0 : forall x, (x^-1 == 0) = (x == 0).

End UnitRingTheory.

Section UnitRingMorphism.

Variables (aR rR : UnitRing.type) (f : aR -> rR).
Hypothesis fM : morphism f.

Lemma ringM_unit : forall x, unit x -> unit (f x).

Lemma ringM_inv : forall x, unit x -> f x^-1 = (f x)^-1.

Lemma ringM_div : forall x y, unit y -> f (x / y) = f x / f y.

End UnitRingMorphism.

Reification of the theory of rings with units, in named style  
Section TermDef.

Variable R : Type.

Inductive term : Type :=
| Var of nat
| Const of R
| NatConst of nat
| Add of term & term
| Opp of term
| NatMul of term & nat
| Mul of term & term
| Inv of term
| Exp of term & nat.

Inductive formula : Type :=
| Bool of bool
| Equal of term & term
| Unit of term
| And of formula & formula
| Or of formula & formula
| Implies of formula & formula
| Not of formula
| Exists of nat & formula
| Forall of nat & formula.

End TermDef.


Implicit Arguments Bool [R].

Notation True := (Bool true).
Notation False := (Bool false).

Local Notation "''X_' i" := (Var _ i) : term_scope.
Local Notation "n %:R" := (NatConst _ n) : term_scope.
Local Notation "x %:T" := (Const x) : term_scope.
Local Notation "0" := 0%:R%T : term_scope.
Local Notation "1" := 1%:R%T : term_scope.
Local Infix "+" := Add : term_scope.
Local Notation "- t" := (Opp t) : term_scope.
Local Notation "t - u" := (Add t (- u)) : term_scope.
Local Infix "*" := Mul : term_scope.
Local Infix "*+" := NatMul : term_scope.
Local Notation "t ^-1" := (Inv t) : term_scope.
Local Notation "t / u" := (Mul t u^-1) : term_scope.
Local Infix "^+" := Exp : term_scope.
Local Infix "==" := Equal : term_scope.
Local Infix "/\" := And : term_scope.
Local Infix "\/" := Or : term_scope.
Local Infix "==>" := Implies : term_scope.
Local Notation "~ f" := (Not f) : term_scope.
Local Notation "x != y" := (Not (x == y)) : term_scope.
Local Notation "''exists' ''X_' i , f" := (Exists i f) : term_scope.
Local Notation "''forall' ''X_' i , f" := (Forall i f) : term_scope.

Section Substitution.

Variable R : Type.

Fixpoint tsubst (t : term R) (s : nat * term R) :=
  match t with
  | 'X_i => if i == s.1 then s.2 else t
  | _%:T | _%:R => t
  | t1 + t2 => tsubst t1 s + tsubst t2 s
  | - t1 => - tsubst t1 s
  | t1 *+ n => tsubst t1 s *+ n
  | t1 * t2 => tsubst t1 s * tsubst t2 s
  | t1^-1 => (tsubst t1 s)^-1
  | t1 ^+ n => tsubst t1 s ^+ n
  end%T.

Fixpoint fsubst (f : formula R) (s : nat * term R) :=
  match f with
  | Bool _ => f
  | t1 == t2 => tsubst t1 s == tsubst t2 s
  | Unit t1 => Unit (tsubst t1 s)
  | f1 /\ f2 => fsubst f1 s /\ fsubst f2 s
  | f1 \/ f2 => fsubst f1 s \/ fsubst f2 s
  | f1 ==> f2 => fsubst f1 s ==> fsubst f2 s
  | ~ f1 => ~ fsubst f1 s
  | ('exists 'X_i, f1) => 'exists 'X_i, if i == s.1 then f1 else fsubst f1 s
  | ('forall 'X_i, f1) => 'forall 'X_i, if i == s.1 then f1 else fsubst f1 s
  end%T.

End Substitution.

Section EvalTerm.

Variable R : UnitRing.type.

Evaluation of a reified term into R a ring with units 
Fixpoint eval (e : seq R) (t : term R) {struct t} : R :=
  match t with
  | ('X_i)%T => e`_i
  | (x%:T)%T => x
  | (n%:R)%T => n%:R
  | (t1 + t2)%T => eval e t1 + eval e t2
  | (- t1)%T => - eval e t1
  | (t1 *+ n)%T => eval e t1 *+ n
  | (t1 * t2)%T => eval e t1 * eval e t2
  | t1^-1%T => (eval e t1)^-1
  | (t1 ^+ n)%T => eval e t1 ^+ n
  end.

Definition same_env (e e' : seq R) := nth 0 e =1 nth 0 e'.

Lemma eq_eval : forall e e' t, same_env e e' -> eval e t = eval e' t.

Lemma eval_tsubst : forall e t s,
  eval e (tsubst t s) = eval (set_nth 0 e s.1 (eval e s.2)) t.

Evaluation of a reified formula 
Fixpoint holds (e : seq R) (f : formula R) {struct f} : Prop :=
  match f with
  | Bool b => b
  | (t1 == t2)%T => eval e t1 = eval e t2
  | Unit t1 => unit (eval e t1)
  | (f1 /\ f2)%T => holds e f1 /\ holds e f2
  | (f1 \/ f2)%T => holds e f1 \/ holds e f2
  | (f1 ==> f2)%T => holds e f1 -> holds e f2
  | (~ f1)%T => ~ holds e f1
  | ('exists 'X_i, f1)%T => exists x, holds (set_nth 0 e i x) f1
  | ('forall 'X_i, f1)%T => forall x, holds (set_nth 0 e i x) f1
  end.

Lemma same_env_sym : forall e e', same_env e e' -> same_env e' e.

Extensionality of formula evaluation 
Lemma eq_holds : forall e e' f, same_env e e' -> holds e f -> holds e' f.

Evaluation and substitution by a constant 
Lemma holds_fsubst : forall e f i v,
  holds e (fsubst f (i, v%:T)%T) <-> holds (set_nth 0 e i v) f.

Boolean test selecting terms in the language of rings 
Fixpoint rterm (t : term R) :=
  match t with
  | _^-1 => false
  | t1 + t2 | t1 * t2 => rterm t1 && rterm t2
  | - t1 | t1 *+ _ | t1 ^+ _ => rterm t1
  | _ => true
  end%T.

Boolean test selecting formulas in the theory of rings 
Fixpoint rformula (f : formula R) :=
  match f with
  | Bool _ => true
  | t1 == t2 => rterm t1 && rterm t2
  | Unit t1 => false
  | f1 /\ f2 | f1 \/ f2 | f1 ==> f2 => rformula f1 && rformula f2
  | ~ f1 | ('exists 'X__, f1) | ('forall 'X__, f1) => rformula f1
  end%T.

Upper bound of the names used in a term 
Fixpoint ub_var (t : term R) :=
  match t with
  | 'X_i => i.+1
  | t1 + t2 | t1 * t2 => maxn (ub_var t1) (ub_var t2)
  | - t1 | t1 *+ _ | t1 ^+ _ | t1^-1 => ub_var t1
  | _ => 0%N
  end%T.

Replaces inverses in the term t by fresh variables, accumulating the 
 substitution. 
Fixpoint to_rterm (t : term R) (r : seq (term R)) (n : nat) {struct t} :=
  match t with
  | t1^-1 =>
    let: (t1', r1) := to_rterm t1 r n in
      ('X_(n + size r1), rcons r1 t1')
  | t1 + t2 =>
    let: (t1', r1) := to_rterm t1 r n in
    let: (t2', r2) := to_rterm t2 r1 n in
      (t1' + t2', r2)
  | - t1 =>
   let: (t1', r1) := to_rterm t1 r n in
     (- t1', r1)
  | t1 *+ m =>
   let: (t1', r1) := to_rterm t1 r n in
     (t1' *+ m, r1)
  | t1 * t2 =>
    let: (t1', r1) := to_rterm t1 r n in
    let: (t2', r2) := to_rterm t2 r1 n in
      (Mul t1' t2', r2)
  | t1 ^+ m =>
       let: (t1', r1) := to_rterm t1 r n in
     (t1' ^+ m, r1)
  | _ => (t, r)
  end%T.

Lemma to_rterm_id : forall t r n, rterm t -> to_rterm t r n = (t, r).

A ring formula stating that t1 is equal to 0 in the ring theory. 
 Also applies to non commutative rings.                           
Definition eq0_rform t1 :=
  let m := ub_var t1 in
  let: (t1', r1) := to_rterm t1 [::] m in
  let fix loop r i := match r with
  | [::] => t1' == 0
  | t :: r' =>
    let f := 'X_i * t == 1 /\ t * 'X_i == 1 in
     'forall 'X_i, (f \/ 'X_i == t /\ ~ ('exists 'X_i, f)) ==> loop r' i.+1
  end%T
  in loop r1 m.

Transformation of a formula in the theory of rings with units into an 
 equivalent formula in the sub-theory of rings.                        
Fixpoint to_rform f :=
  match f with
  | Bool b => f
  | t1 == t2 => eq0_rform (t1 - t2)
  | Unit t1 => eq0_rform (t1 * t1^-1 - 1)
  | f1 /\ f2 => to_rform f1 /\ to_rform f2
  | f1 \/ f2 => to_rform f1 \/ to_rform f2
  | f1 ==> f2 => to_rform f1 ==> to_rform f2
  | ~ f1 => ~ to_rform f1
  | ('exists 'X_i, f1) => 'exists 'X_i, to_rform f1
  | ('forall 'X_i, f1) => 'forall 'X_i, to_rform f1
  end%T.

The transformation gives a ring formula. 
Lemma to_rform_rformula : forall f, rformula (to_rform f).

Correctness of the transformation. 
Lemma to_rformP : forall e f, holds e (to_rform f) <-> holds e f.

Boolean test selecting formulas which describe a constructable set, 
 i.e. formulas without quantifiers.                                  

The quantifier elimination check. 
Fixpoint qf_form (f : formula R) :=
  match f with
  | Bool _ | _ == _ | Unit _ => true
  | f1 /\ f2 | f1 \/ f2 | f1 ==> f2 => qf_form f1 && qf_form f2
  | ~ f1 => qf_form f1
  | _ => false
  end%T.

Boolean holds predicate for quantifier free formulas 
Definition qf_eval e := fix loop (f : formula R) : bool :=
  match f with
  | Bool b => b
  | t1 == t2 => (eval e t1 == eval e t2)%bool
  | Unit t1 => unit (eval e t1)
  | f1 /\ f2 => loop f1 && loop f2
  | f1 \/ f2 => loop f1 || loop f2
  | f1 ==> f2 => (loop f1 ==> loop f2)%bool
  | ~ f1 => ~~ loop f1
  |_ => false
  end%T.

qf_eval is equivalent to holds 
Lemma qf_evalP : forall e f, qf_form f -> reflect (holds e f) (qf_eval e f).

Implicit Type bc : seq (term R) * seq (term R).

Quantifier-free formula are normalized into DNF. A DNF is 
 represented by the type seq (seq (term R) * seq (term R)), where we 
 separate positive and negative literals 

DNF preserving conjunction 
Definition and_dnf bcs1 bcs2 :=
  \big[cat/nil]_(bc1 <- bcs1)
     map (fun bc2 => (bc1.1 ++ bc2.1, bc1.2 ++ bc2.2)) bcs2.

Computes a DNF from a qf ring formula 
Fixpoint qf_to_dnf (f : formula R) (neg : bool) {struct f} :=
  match f with
  | Bool b => if b (+) neg then [:: ([::], [::])] else [::]
  | t1 == t2 => [:: if neg then ([::], [:: t1 - t2]) else ([:: t1 - t2], [::])]
  | f1 /\ f2 => (if neg then cat else and_dnf) [rec f1, neg] [rec f2, neg]
  | f1 \/ f2 => (if neg then and_dnf else cat) [rec f1, neg] [rec f2, neg]
  | f1 ==> f2 => (if neg then and_dnf else cat) [rec f1, ~~ neg] [rec f2, neg]
  | ~ f1 => [rec f1, ~~ neg]
  | _ => if neg then [:: ([::], [::])] else [::]
  end%T where "[ 'rec' f , neg ]" := (qf_to_dnf f neg).

Conversely, transforms a DNF into a formula 
Definition dnf_to_form :=
  let pos_lit t := And (t == 0) in let neg_lit t := And (t != 0) in
  let cls bc := Or (foldr pos_lit True bc.1 /\ foldr neg_lit True bc.2) in
  foldr cls False.

Catenation of dnf is the Or of formulas 
Lemma cat_dnfP : forall e bcs1 bcs2,
  qf_eval e (dnf_to_form (bcs1 ++ bcs2))
    = qf_eval e (dnf_to_form bcs1 \/ dnf_to_form bcs2).

and_dnf is the And of formulas 
Lemma and_dnfP : forall e bcs1 bcs2,
  qf_eval e (dnf_to_form (and_dnf bcs1 bcs2))
   = qf_eval e (dnf_to_form bcs1 /\ dnf_to_form bcs2).

Lemma qf_to_dnfP : forall e,
  let qev f b := qf_eval e (dnf_to_form (qf_to_dnf f b)) in
  forall f, qf_form f && rformula f -> qev f false = qf_eval e f.

Lemma dnf_to_form_qf : forall bcs, qf_form (dnf_to_form bcs).

Definition dnf_rterm cl := all rterm cl.1 && all rterm cl.2.

Lemma qf_to_dnf_rterm : forall f b, rformula f -> all dnf_rterm (qf_to_dnf f b).

Lemma dnf_to_rform : forall bcs, rformula (dnf_to_form bcs) = all dnf_rterm bcs.

Section Pick.

Variables (I : finType) (pred_f then_f : I -> formula R) (else_f : formula R).

Definition Pick :=
  \big[Or/False]_(p : {ffun pred I})
    ((\big[And/True]_i (if p i then pred_f i else ~ pred_f i))
    /\ (if pick p is Some i then then_f i else else_f))%T.

Lemma Pick_form_qf :
   (forall i, qf_form (pred_f i)) ->
   (forall i, qf_form (then_f i)) ->
    qf_form else_f ->
  qf_form Pick.

Lemma eval_Pick : forall e (qev := qf_eval e),
  let P i := qev (pred_f i) in
  qev Pick = (if pick P is Some i then qev (then_f i) else qev else_f).

End Pick.

Section MultiQuant.

Variable f : formula R.
Implicit Type I : seq nat.
Implicit Type e : seq R.

Lemma foldExistsP : forall I e,
  (exists2 e', {in [predC I], same_env e e'} & holds e' f)
    <-> holds e (foldr Exists f I).

Lemma foldForallP : forall I e,
  (forall e', {in [predC I], same_env e e'} -> holds e' f)
    <-> holds e (foldr Forall f I).

End MultiQuant.

End EvalTerm.


Module ComUnitRing.

Record class_of (R : Type) : Type := Class {
  base1 :> ComRing.class_of R;
  ext :> UnitRing.mixin_of (Ring.Pack base1 R)
}.

Coercion base2 R m := UnitRing.Class (@ext R m).

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.

Section Mixin.

Variables (R : ComRing.type) (unit : pred R) (inv : R -> R).
Hypothesis mulVx : {in unit, left_inverse 1 inv *%R}.
Hypothesis unitPl : forall x y, y * x = 1 -> unit x.

Lemma mulC_mulrV : {in unit, right_inverse 1 inv *%R}.

Lemma mulC_unitP : forall x y, y * x = 1 /\ x * y = 1 -> unit x.

Definition Mixin := UnitRing.EtaMixin mulVx mulC_mulrV mulC_unitP.

End Mixin.

Definition pack T :=
  fun bT b & phant_id (ComRing.class bT) (b : ComRing.class_of T) =>
  fun mT m & phant_id (UnitRing.class mT) (@UnitRing.Class T b m) =>
  Pack (@Class T b m) T.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.
Coercion comRingType cT := ComRing.Pack (class cT) cT.
Coercion unitRingType cT := UnitRing.Pack (class cT) cT.
Definition com_unitRingType cT :=
  @UnitRing.Pack (comRingType cT) (class cT) cT.

End ComUnitRing.

Canonical Structure ComUnitRing.eqType.
Canonical Structure ComUnitRing.choiceType.
Canonical Structure ComUnitRing.zmodType.
Canonical Structure ComUnitRing.ringType.
Canonical Structure ComUnitRing.unitRingType.
Canonical Structure ComUnitRing.comRingType.

Section ComUnitRingTheory.

Variable R : ComUnitRing.type.
Implicit Types x y : R.

Lemma unitr_mul : forall x y, unit (x * y) = unit x && unit y.

End ComUnitRingTheory.

Module IntegralDomain.

Definition axiom (R : Ring.type) :=
  forall x y : R, x * y = 0 -> (x == 0) || (y == 0).

Record class_of (R : Type) : Type :=
  Class {base :> ComUnitRing.class_of R; ext : axiom (Ring.Pack base R)}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
  fun bT b & phant_id (ComUnitRing.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.
Coercion comRingType cT := ComRing.Pack (class cT) cT.
Coercion unitRingType cT := UnitRing.Pack (class cT) cT.
Coercion comUnitRingType cT := ComUnitRing.Pack (class cT) cT.

End IntegralDomain.

Canonical Structure IntegralDomain.eqType.
Canonical Structure IntegralDomain.choiceType.
Canonical Structure IntegralDomain.zmodType.
Canonical Structure IntegralDomain.ringType.
Canonical Structure IntegralDomain.unitRingType.
Canonical Structure IntegralDomain.comRingType.
Canonical Structure IntegralDomain.comUnitRingType.

Section IntegralDomainTheory.

Variable R : IntegralDomain.type.
Implicit Types x y : R.

Lemma mulf_eq0 : forall x y, (x * y == 0) = (x == 0) || (y == 0).

Lemma mulf_neq0 : forall x y, x != 0 -> y != 0 -> x * y != 0.

Lemma expf_eq0 : forall x n, (x ^+ n == 0) = (n > 0) && (x == 0).

Lemma expf_neq0 : forall x m, x != 0 -> x ^+ m != 0.

Lemma mulfI : forall x, x != 0 -> injective ( *%R x).

Lemma mulIf : forall x, x != 0 -> injective ( *%R^~ x).

End IntegralDomainTheory.

Module Field.

Definition mixin_of (F : UnitRing.type) := forall x : F, x != 0 -> unit x.

Record class_of (F : Type) : Type := Class {
  base :> IntegralDomain.class_of F;
  ext: mixin_of (UnitRing.Pack base F)
}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) :=
  fun bT b & phant_id (IntegralDomain.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Lemma IdomainMixin : forall R, mixin_of R -> IntegralDomain.axiom R.

Section Mixins.

Variables (R : ComRing.type) (inv : R -> R).

Definition axiom := forall x, x != 0 -> inv x * x = 1.
Hypothesis mulVx : axiom.
Hypothesis inv0 : inv 0 = 0.

Lemma intro_unit : forall x y : R, y * x = 1 -> x != 0.

Lemma inv_out : {in predC (predC1 0), inv =1 id}.

Definition UnitMixin := ComUnitRing.Mixin mulVx intro_unit inv_out.

Lemma Mixin : mixin_of (UnitRing.Pack (UnitRing.Class UnitMixin) R).

End Mixins.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.
Coercion comRingType cT := ComRing.Pack (class cT) cT.
Coercion unitRingType cT := UnitRing.Pack (class cT) cT.
Coercion comUnitRingType cT := ComUnitRing.Pack (class cT) cT.
Coercion idomainType cT := IntegralDomain.Pack (class cT) cT.

End Field.

Canonical Structure Field.eqType.
Canonical Structure Field.choiceType.
Canonical Structure Field.zmodType.
Canonical Structure Field.ringType.
Canonical Structure Field.unitRingType.
Canonical Structure Field.comRingType.
Canonical Structure Field.comUnitRingType.
Canonical Structure Field.idomainType.

Section FieldTheory.

Variable F : Field.type.
Implicit Types x y : F.

Lemma unitfE : forall x, unit x = (x != 0).

Lemma mulVf : forall x, x != 0 -> x^-1 * x = 1.
Lemma divff : forall x, x != 0 -> x / x = 1.
Definition mulfV := divff.
Lemma mulKf : forall x, x != 0 -> cancel ( *%R x) ( *%R x^-1).
Lemma mulVKf : forall x, x != 0 -> cancel ( *%R x^-1) ( *%R x).
Lemma mulfK : forall x, x != 0 -> cancel ( *%R^~ x) ( *%R^~ x^-1).
Lemma mulfVK : forall x, x != 0 -> cancel ( *%R^~ x^-1) ( *%R^~ x).
Definition divfK := mulfVK.

Lemma invf_mul : {morph (fun x => x^-1) : x y / x * y}.

Lemma prodf_inv : forall I r (P : pred I) (E : I -> F),
  \prod_(i <- r | P i) (E i)^-1 = (\prod_(i <- r | P i) E i)^-1.

Lemma natf0_char : forall n,
  n > 0 -> n%:R == 0 :> F -> exists p, p \in [char F].

Lemma charf'_nat : forall n, [char F]^'.-nat n = (n%:R != 0 :> F).

Lemma charf0P : [char F] =i pred0 <-> (forall n, (n%:R == 0 :> F) = (n == 0)%N).

Section FieldMorphismInj.

Variables (R : Ring.type) (f : F -> R).
Hypothesis fRM : morphism f.

Lemma fieldM_eq0 : forall x, (f x == 0) = (x == 0).

Lemma fieldM_inj : injective f.

Lemma fieldM_char : [char R] =i [char F].

End FieldMorphismInj.

Section FieldMorphismInv.

Variables (R : UnitRing.type) (f : F -> R).
Hypothesis fRM : morphism f.

Lemma fieldM_unit : forall x, unit (f x) = (x != 0).

Lemma fieldM_inv : {morph f: x / x^-1}.

Lemma fieldM_div : {morph f : x y / x / y}.

End FieldMorphismInv.

End FieldTheory.

Module DecidableField.

Definition axiom (R : UnitRing.type) (s : seq R -> pred (formula R)) :=
  forall e f, reflect (holds e f) (s e f).

Record mixin_of (R : UnitRing.type) : Type :=
  Mixin { sat : seq R -> pred (formula R); satP : axiom sat}.

Record class_of (F : Type) : Type :=
  Class {base :> Field.class_of F; mixin:> mixin_of (UnitRing.Pack base F)}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) :=
  fun bT b & phant_id (Field.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Ultimately, there should be a QE Mixin constructor 

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.
Coercion comRingType cT := ComRing.Pack (class cT) cT.
Coercion unitRingType cT := UnitRing.Pack (class cT) cT.
Coercion comUnitRingType cT := ComUnitRing.Pack (class cT) cT.
Coercion idomainType cT := IntegralDomain.Pack (class cT) cT.
Coercion fieldType cT := Field.Pack (class cT) cT.

End DecidableField.

Canonical Structure DecidableField.eqType.
Canonical Structure DecidableField.choiceType.
Canonical Structure DecidableField.zmodType.
Canonical Structure DecidableField.ringType.
Canonical Structure DecidableField.unitRingType.
Canonical Structure DecidableField.comRingType.
Canonical Structure DecidableField.comUnitRingType.
Canonical Structure DecidableField.idomainType.
Canonical Structure DecidableField.fieldType.

Section DecidableFieldTheory.

Variable F : DecidableField.type.

Definition sat := DecidableField.sat (DecidableField.class F).

Lemma satP : DecidableField.axiom sat.

Lemma sol_subproof : forall n f,
  reflect (exists s, (size s == n) && sat s f)
          (sat [::] (foldr Exists f (iota 0 n))).

Definition sol n f :=
  if sol_subproof n f is ReflectT sP then xchoose sP else nseq n 0.

Lemma size_sol : forall n f, size (sol n f) = n.

Lemma solP : forall n f,
  reflect (exists2 s, size s = n & holds s f) (sat (sol n f) f).

Lemma eq_sat : forall f1 f2,
  (forall e, holds e f1 <-> holds e f2) -> sat^~ f1 =1 sat^~ f2.

Lemma eq_sol : forall f1 f2,
  (forall e, holds e f1 <-> holds e f2) -> sol^~ f1 =1 sol^~ f2.

End DecidableFieldTheory.

Implicit Arguments satP [F e f].
Implicit Arguments solP [F n f].

Structure of field with quantifier elimination 
Module QE.

Section Axioms.

Variable R : UnitRing.type.
Variable proj : nat -> seq (term R) * seq (term R) -> formula R.
proj is the elimination of a single existential quantifier 

Definition wf_proj_axiom :=
  forall i bc (bc_i := proj i bc),
    dnf_rterm bc -> qf_form bc_i && rformula bc_i : Prop.

The elimination operator p preserves  validity 
Definition holds_proj_axiom :=
  forall i bc (ex_i_bc := ('exists 'X_i, dnf_to_form [:: bc])%T) e,
  dnf_rterm bc -> reflect (holds e ex_i_bc) (qf_eval e (proj i bc)).

End Axioms.

Record mixin_of (R : UnitRing.type) : Type := Mixin {
  proj : nat -> (seq (term R) * seq (term R)) -> formula R;
  wf_proj : wf_proj_axiom proj;
  holds_proj : holds_proj_axiom proj
}.

Record class_of (F : Type) : Type :=
  Class {base :> Field.class_of F; mixin:> mixin_of (UnitRing.Pack base F)}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T b0 (m0 : mixin_of (@UnitRing.Pack T b0 T)) :=
  fun bT b & phant_id (Field.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.
Coercion comRingType cT := ComRing.Pack (class cT) cT.
Coercion unitRingType cT := UnitRing.Pack (class cT) cT.
Coercion comUnitRingType cT := ComUnitRing.Pack (class cT) cT.
Coercion idomainType cT := IntegralDomain.Pack (class cT) cT.
Coercion fieldType cT := Field.Pack (class cT) cT.

End QE.

Canonical Structure QE.eqType.
Canonical Structure QE.choiceType.
Canonical Structure QE.zmodType.
Canonical Structure QE.ringType.
Canonical Structure QE.unitRingType.
Canonical Structure QE.comRingType.
Canonical Structure QE.comUnitRingType.
Canonical Structure QE.idomainType.
Canonical Structure QE.fieldType.

Section QE_theory.

Variable F : QE.type.

Definition proj := QE.proj (QE.class F).

Lemma wf_proj : QE.wf_proj_axiom proj.

Lemma holds_proj : QE.holds_proj_axiom proj.

Implicit Type f : formula F.

Let elim_aux f n := foldr Or False (map (proj n) (qf_to_dnf f false)).

Fixpoint quantifier_elim (f : formula F) : formula F :=
  match f with
  | f1 /\ f2 => (quantifier_elim f1) /\ (quantifier_elim f2)
  | f1 \/ f2 => (quantifier_elim f1) \/ (quantifier_elim f2)
  | f1 ==> f2 => (~ quantifier_elim f1) \/ (quantifier_elim f2)
  | ~ f => ~ quantifier_elim f
  | ('exists 'X_n, f) => elim_aux (quantifier_elim f) n
  | ('forall 'X_n, f) => ~ elim_aux (~ quantifier_elim f) n
  | _ => f
  end%T.

Lemma quantifier_elim_wf : forall f (qf := quantifier_elim f),
  rformula f -> qf_form qf && rformula qf.

Lemma quantifier_elim_rformP : forall e f,
  rformula f -> reflect (holds e f) (qf_eval e (quantifier_elim f)).

Definition proj_sat e f := qf_eval e (quantifier_elim (to_rform f)).

Lemma proj_satP : DecidableField.axiom proj_sat.

Definition QEDecidableFieldMixin := DecidableField.Mixin proj_satP.

Canonical Structure QEDecidableField :=
  DecidableField.Pack (DecidableField.Class QEDecidableFieldMixin) F.

End QE_theory.

Module ClosedField.

Axiom == all non-constant monic polynomials have a root 
Definition axiom (R : Ring.type) :=
  forall n (P : nat -> R), n > 0 ->
   exists x : R, x ^+ n = \sum_(i < n) P i * (x ^+ i).

Record class_of (F : Type) : Type :=
  Class {base :> DecidableField.class_of F; _ : axiom (Ring.Pack base F)}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition clone T cT c of phant_id (class cT) c := @Pack T c T.

Definition pack T b0 (m0 : axiom (@Ring.Pack T b0 T)) :=
  fun bT b & phant_id (DecidableField.class bT) b =>
  fun m & phant_id m0 m => Pack (@Class T b m) T.

There should eventually be a constructor from polynomial resolution 
 that builds the DecidableField mixin using QE.                      

Coercion eqType cT := Equality.Pack (class cT) cT.
Coercion choiceType cT := Choice.Pack (class cT) cT.
Coercion zmodType cT := Zmodule.Pack (class cT) cT.
Coercion ringType cT := Ring.Pack (class cT) cT.
Coercion comRingType cT := ComRing.Pack (class cT) cT.
Coercion unitRingType cT := UnitRing.Pack (class cT) cT.
Coercion comUnitRingType cT := ComUnitRing.Pack (class cT) cT.
Coercion idomainType cT := IntegralDomain.Pack (class cT) cT.
Coercion fieldType cT := Field.Pack (class cT) cT.
Coercion decFieldType cT := DecidableField.Pack (class cT) cT.

End ClosedField.

Canonical Structure ClosedField.eqType.
Canonical Structure ClosedField.choiceType.
Canonical Structure ClosedField.zmodType.
Canonical Structure ClosedField.ringType.
Canonical Structure ClosedField.unitRingType.
Canonical Structure ClosedField.comRingType.
Canonical Structure ClosedField.comUnitRingType.
Canonical Structure ClosedField.idomainType.
Canonical Structure ClosedField.fieldType.
Canonical Structure ClosedField.decFieldType.


Section ClosedFieldTheory.

Variable F : ClosedField.type.

Lemma solve_monicpoly : ClosedField.axiom F.

End ClosedFieldTheory.

Module Lmodule.

Section Lmodule.

Variable R : Ring.type.
Implicit Type phR : phant R.

Structure mixin_of (M : Zmodule.type) : Type := Mixin {
  scale : R -> M -> M;
  _ : forall a b m, scale a (scale b m) = scale (a * b) m;
  _ : left_id 1 scale;
  _ : forall a, {morph scale a : m n / m + n};
  _ : forall m, {morph scale^~ m : a b / a + b}
}.

Structure class_of M := Class {
  base :> Zmodule.class_of M;
  ext :> mixin_of (Zmodule.Pack base M)
}.

Structure type phR := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class phR (cT : type phR) :=
  let: Pack _ c _ := cT return class_of cT in c.
Definition clone phR T cT c of phant_id (@class phR cT) c := @Pack phR T c T.
Definition pack phR T b0 (m0 : mixin_of (@Zmodule.Pack T b0 T)) :=
  fun bT b & phant_id (Zmodule.class bT) b =>
  fun m & phant_id m0 m => Pack phR (@Class T b m) T.

Coercion eqType phR cT := Equality.Pack (@class phR cT) cT.
Coercion choiceType phR cT := Choice.Pack (@class phR cT) cT.
Coercion zmodType phR cT := Zmodule.Pack (@class phR cT) cT.

End Lmodule.

End Lmodule.

Canonical Structure Lmodule.eqType.
Canonical Structure Lmodule.choiceType.
Canonical Structure Lmodule.zmodType.

Definition scale R (M : @Lmodule.type R (Phant R)) : R -> M -> M :=
  Lmodule.scale (Lmodule.class M).

Local Notation "*:%R" := (@scale _ _) : ring_scope.
Local Notation "a *: m" := (scale a m) (at level 40) : ring_scope.

Section LmoduleTheory.

Variable (R : Ring.type) (M : Lmodule.type (Phant R)).
Implicit Type a b c : R.
Implicit Type m : M.

Lemma scalerA : forall a b m, a *: (b *: m) = a * b *: m.

Lemma scale1r : @left_id R M 1 *:%R.

Lemma scaler_addr : forall a, {morph (scale a : M -> M) : x y / x + y}.

Lemma scaler_addl : forall m, {morph (@scale _ _)^~ m : a b / a + b}.

Lemma scale0r : forall m, 0 *: m = 0.

Lemma scaler0 : forall a, a *: 0 = 0 :> M.

Lemma scaleNr : forall a m, - a *: m = - (a *: m).

Lemma scaleN1r : forall m, (- 1) *: m = - m.

Lemma scalerN : forall a m, a *: (- m) = - (a *: m).

Lemma scaler_subl : forall a b m, (a - b) *: m = a *: m - b *: m.

Lemma scaler_subr : forall a m1 m2, a *: (m1 - m2) = a *: m1 - a *: m2.

Lemma scaler_nat : forall n m, n%:R *: m = m *+ n.

Lemma scaler_suml : forall m I r (P : pred I) F,
 (\sum_(i <- r | P i) F i) *: m = \sum_(i <- r | P i) F i *: m.

Lemma scaler_sumr : forall a I r (P : pred I) (F : I -> M),
   a *: (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) a *: F i.

End LmoduleTheory.

Module NCalgebra.

Section NCalgebra.

Variable R : Ring.type.
Implicit Type phR : phant R.

Notation scale T L := (@scale R (@Lmodule.pack _ (Phant R) T _ L _ _ id _ id)).
Definition axiom (T: Ring.type) (L: Lmodule.mixin_of R T) :=
  forall k x y, scale T L k (x * y) = scale T L k x * y.

Record class_of (T : Type) : Type := Class {
  base1 :> Ring.class_of T;
  mixin :> Lmodule.mixin_of R (Zmodule.Pack base1 T);
  ext : @axiom (Ring.Pack base1 T) mixin
}.

Coercion base2 R m := Lmodule.Class (@mixin R m).

Structure type phR := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class phR (cT : type phR) :=
  let: Pack _ c _ := cT return class_of cT in c.
Definition clone phR T cT c of phant_id (@class phR cT) c := @Pack phR T c T.
Definition pack phR T b0 m0 (axT: @axiom (@Ring.Pack T b0 T) m0) :=
  fun bT b & phant_id (Ring.class bT) (b : Ring.class_of T) =>
  fun mT m & phant_id (@Lmodule.class R phR mT) (@Lmodule.Class R T b m) =>
  fun ax & phant_id axT ax =>
  Pack (Phant R) (@Class T b m ax) T.

Coercion eqType phR cT := Equality.Pack (@class phR cT) cT.
Coercion choiceType phR cT := Choice.Pack (@class phR cT) cT.
Coercion zmodType phR cT := Zmodule.Pack (@class phR cT) cT.
Coercion ringType phR cT := Ring.Pack (@class phR cT) cT.
Coercion lmoduleType phR cT := Lmodule.Pack phR (@class phR cT) cT.

Definition lmod_ringType phR cT :=
  @Lmodule.Pack R phR (Ring.sort (@ringType phR cT)) (base2 (class cT)) (Ring.sort (ringType cT)).


End NCalgebra.

End NCalgebra.

Canonical Structure NCalgebra.eqType.
Canonical Structure NCalgebra.choiceType.
Canonical Structure NCalgebra.zmodType.
Canonical Structure NCalgebra.ringType.
Canonical Structure NCalgebra.lmoduleType.

Section NCalgebraTheory.

Variable R : Ring.type.
Variable A : NCalgebra.type (Phant R).
Implicit Types k: R.
Implicit Types x y: A.

Lemma scaler_mull: forall k x y, k *: (x * y) = k *: x * y.

Lemma morph_sunit: morphism (fun k => k *: (1: A)).

End NCalgebraTheory.

Module Algebra.

Section Algebra.

Variable R : Ring.type.
Implicit Type phR : phant R.


Definition axiom T1 T2 (scalop: T1->T2->T2) (mulop: T2->T2->T2) :=
               forall k x y, (scalop k (mulop x y)) = (mulop x (scalop k y)) .


Record class_of (T : Type) : Type :=
  Class {base :> NCalgebra.class_of R T;
         _ : axiom (Lmodule.scale (NCalgebra.mixin base)) (Ring.mul (NCalgebra.base1 base))}.

Coercion base2 b   c A := Lmodule.Class (@NCalgebra.mixin b c A).

Structure type phR :Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class phR (cT : type phR) :=
  let: Pack _ c _ := cT return class_of cT in c.
Definition clone phR T cT c of phant_id (@class phR cT) c := @Pack phR T c T.

 Definition pack phR T scale0 mul0 (axT : @axiom R T scale0 mul0) :=
  fun bT b & phant_id (@NCalgebra.class R phR bT) b =>
  fun ax & phant_id axT ax => Pack phR (@Class T b ax) T.


Coercion eqType phR cT := Equality.Pack (@class phR cT) cT.
Coercion choiceType phR cT := Choice.Pack (@class phR cT) cT.
Coercion zmodType phR cT := Zmodule.Pack (@class phR cT) cT.
Coercion ringType phR cT := Ring.Pack (@class phR cT) cT.
Coercion lmoduleType phR cT := Lmodule.Pack phR (@class phR cT) cT.
Coercion ncalgebraType phR cT := NCalgebra.Pack phR (@class phR cT) cT.

End Algebra.

End Algebra.

Canonical Structure Algebra.eqType.
Canonical Structure Algebra.choiceType.
Canonical Structure Algebra.zmodType.
Canonical Structure Algebra.ringType.
Canonical Structure Algebra.lmoduleType.
Canonical Structure Algebra.ncalgebraType.


Section AlgebraTheory.

Variable R : Ring.type.
Variable A : Algebra.type (Phant R).
Implicit Types k: R.
Implicit Types x y: A.

Lemma scaler_com: forall (k:R) (x y:A) , k *: (x * y) = x * (k *: y).

End AlgebraTheory.

Module Theory.

Definition addrA := addrA.
Definition addrC := addrC.
Definition add0r := add0r.
Definition addNr := addNr.
Definition addr0 := addr0.
Definition addrN := addrN.
Definition subrr := subrr.
Definition addrCA := addrCA.
Definition addrAC := addrAC.
Definition addKr := addKr.
Definition addNKr := addNKr.
Definition addrK := addrK.
Definition addrNK := addrNK.
Definition subrK := subrK.
Definition addrI := addrI.
Definition addIr := addIr.
Definition opprK := opprK.
Definition oppr0 := oppr0.
Definition oppr_eq0 := oppr_eq0.
Definition oppr_add := oppr_add.
Definition oppr_sub := oppr_sub.
Definition subr0 := subr0.
Definition sub0r := sub0r.
Definition subr_eq := subr_eq.
Definition subr_eq0 := subr_eq0.
Definition sumr_opp := sumr_opp.
Definition sumr_sub := sumr_sub.
Definition sumr_muln := sumr_muln.
Definition sumr_muln_r := sumr_muln_r.
Definition sumr_const := sumr_const.
Definition mulr0n := mulr0n.
Definition mulrS := mulrS.
Definition mulr1n := mulr1n.
Definition mulrSr := mulrSr.
Definition mulrb := mulrb.
Definition mul0rn := mul0rn.
Definition oppr_muln := oppr_muln.
Definition mulrn_addl := mulrn_addl.
Definition mulrn_addr := mulrn_addr.
Definition mulrnA := mulrnA.
Definition mulrnAC := mulrnAC.
Definition mulrA := mulrA.
Definition mul1r := mul1r.
Definition mulr1 := mulr1.
Definition mulr_addl := mulr_addl.
Definition mulr_addr := mulr_addr.
Definition nonzero1r := nonzero1r.
Definition oner_eq0 := oner_eq0.
Definition mul0r := mul0r.
Definition mulr0 := mulr0.
Definition mulrN := mulrN.
Definition mulNr := mulNr.
Definition mulrNN := mulrNN.
Definition mulN1r := mulN1r.
Definition mulrN1 := mulrN1.
Definition mulr_subl := mulr_subl.
Definition mulr_subr := mulr_subr.
Definition mulrnAl := mulrnAl.
Definition mulrnAr := mulrnAr.
Definition mulr_natl := mulr_natl.
Definition mulr_natr := mulr_natr.
Definition natr_add := natr_add.
Definition natr_mul := natr_mul.
Definition natr_exp := natr_exp.
Definition expr0 := expr0.
Definition exprS := exprS.
Definition expr1 := expr1.
Definition exp1rn := exp1rn.
Definition exprn_addr := exprn_addr.
Definition exprSr := exprSr.
Definition commr_sym := commr_sym.
Definition commr_refl := commr_refl.
Definition commr0 := commr0.
Definition commr1 := commr1.
Definition commr_opp := commr_opp.
Definition commrN1 := commrN1.
Definition commr_add := commr_add.
Definition commr_muln := commr_muln.
Definition commr_mul := commr_mul.
Definition commr_nat := commr_nat.
Definition commr_exp := commr_exp.
Definition commr_exp_mull := commr_exp_mull.
Definition commr_sign := commr_sign.
Definition exprn_mulnl := exprn_mulnl.
Definition exprn_mulr := exprn_mulr.
Definition signr_odd := signr_odd.
Definition signr_eq0 := signr_eq0.
Definition signr_addb := signr_addb.
Definition exprN := exprN.
Definition exprn_addl_comm := exprn_addl_comm.
Definition exprn_subl_comm := exprn_subl_comm.
Definition subr_expn_comm := subr_expn_comm.
Definition subr_expn_1 := subr_expn_1.
Definition charf0 := charf0.
Definition charf_prime := charf_prime.
Definition dvdn_charf := dvdn_charf.
Definition charf_eq := charf_eq.
Definition bin_lt_charf_0 := bin_lt_charf_0.
Definition Frobenius_autE := Frobenius_autE.
Definition Frobenius_aut_0 := Frobenius_aut_0.
Definition Frobenius_aut_1 := Frobenius_aut_1.
Definition Frobenius_aut_add_comm := Frobenius_aut_add_comm.
Definition Frobenius_aut_muln := Frobenius_aut_muln.
Definition Frobenius_aut_nat := Frobenius_aut_nat.
Definition Frobenius_aut_mul_comm := Frobenius_aut_mul_comm.
Definition Frobenius_aut_exp := Frobenius_aut_exp.
Definition Frobenius_aut_opp := Frobenius_aut_opp.
Definition Frobenius_aut_sub_comm := Frobenius_aut_sub_comm.
Definition prodr_const := prodr_const.
Definition mulrC := mulrC.
Definition mulrCA := mulrCA.
Definition mulrAC := mulrAC.
Definition exprn_mull := exprn_mull.
Definition prodr_exp := prodr_exp.
Definition prodr_exp_r := prodr_exp_r.
Definition prodr_opp := prodr_opp.
Definition exprn_addl := exprn_addl.
Definition exprn_subl := exprn_subl.
Definition subr_expn := subr_expn.
Definition mulrV := mulrV.
Definition divrr := divrr.
Definition mulVr := mulVr.
Definition invr_out := invr_out.
Definition unitrP := unitrP.
Definition mulKr := mulKr.
Definition mulVKr := mulVKr.
Definition mulrK := mulrK.
Definition mulrVK := mulrVK.
Definition divrK := divrK.
Definition mulrI := mulrI.
Definition mulIr := mulIr.
Definition commr_inv := commr_inv.
Definition unitrE := unitrE.
Definition invrK := invrK.
Definition invr_inj := invr_inj.
Definition unitr_inv := unitr_inv.
Definition unitr1 := unitr1.
Definition invr1 := invr1.
Definition unitr0 := unitr0.
Definition invr0 := invr0.
Definition unitr_opp := unitr_opp.
Definition invrN := invrN.
Definition unitr_mull := unitr_mull.
Definition unitr_mulr := unitr_mulr.
Definition invr_mul := invr_mul.
Definition invr_eq0 := invr_eq0.
Definition invr_neq0 := invr_neq0.
Definition commr_unit_mul := commr_unit_mul.
Definition unitr_exp := unitr_exp.
Definition unitr_pexp := unitr_pexp.
Definition expr_inv := expr_inv.
Definition eq_eval := eq_eval.
Definition eval_tsubst := eval_tsubst.
Definition eq_holds := eq_holds.
Definition holds_fsubst := holds_fsubst.
Definition unitr_mul := unitr_mul.
Definition mulf_eq0 := mulf_eq0.
Definition mulf_neq0 := mulf_neq0.
Definition expf_eq0 := expf_eq0.
Definition expf_neq0 := expf_neq0.
Definition mulfI := mulfI.
Definition mulIf := mulIf.
Definition unitfE := unitfE.
Definition mulVf := mulVf.
Definition mulfV := mulfV.
Definition divff := divff.
Definition mulKf := mulKf.
Definition mulVKf := mulVKf.
Definition mulfK := mulfK.
Definition mulfVK := mulfVK.
Definition divfK := divfK.
Definition invf_mul := invf_mul.
Definition prodf_inv := prodf_inv.
Definition natf0_char := natf0_char.
Definition charf'_nat := charf'_nat.
Definition charf0P := charf0P.
Definition satP := @satP.
Definition eq_sat := eq_sat.
Definition solP := @solP.
Definition eq_sol := eq_sol.
Definition size_sol := size_sol.
Definition solve_monicpoly := solve_monicpoly.
Definition ringM_sub := ringM_sub.
Definition ringM_0 := ringM_0.
Definition ringM_1 := ringM_1.
Definition ringM_opp := ringM_opp.
Definition ringM_add := ringM_add.
Definition ringM_sum := ringM_sum.
Definition ringM_mul := ringM_mul.
Definition ringM_prod := ringM_prod.
Definition ringM_natmul := ringM_natmul.
Definition ringM_nat := ringM_nat.
Definition ringM_exp := ringM_exp.
Definition ringM_sign := ringM_sign.
Definition ringM_char := ringM_char.
Definition comp_ringM := comp_ringM.
Definition ringM_isom := ringM_isom.
Definition ringM_comm := ringM_comm.
Definition ringM_unit := ringM_unit.
Definition Frobenius_aut_RM := Frobenius_aut_RM.
Definition fieldM_eq0 := fieldM_eq0.
Definition fieldM_inj := fieldM_inj.
Definition ringM_inv := ringM_inv.
Definition fieldM_char := fieldM_char.
Definition ringM_div := ringM_div.
Definition fieldM_unit := fieldM_unit.
Definition fieldM_inv := fieldM_inv.
Definition fieldM_div := fieldM_div.
Definition scalerA := scalerA.
Definition scale1r := scale1r.
Definition scaler_addr := scaler_addr.
Definition scaler_addl := scaler_addl.
Definition scaler0 := scaler0.
Definition scale0r := scale0r.
Definition scaleNr := scaleNr.
Definition scaleN1r := scaleN1r.
Definition scalerN := scalerN.
Definition scaler_subl := scaler_subl.
Definition scaler_subr := scaler_subr.
Definition scaler_nat := scaler_nat.
Definition scaler_suml := scaler_suml.
Definition scaler_sumr := scaler_sumr.
Definition scaler_mull := scaler_mull.
Definition morph_sunit := morph_sunit.

Implicit Arguments satP [F e f].
Implicit Arguments solP [F n f].

End Theory.

End GRing.

Canonical Structure GRing.Zmodule.eqType.
Canonical Structure GRing.Zmodule.choiceType.
Canonical Structure GRing.Ring.eqType.
Canonical Structure GRing.Ring.choiceType.
Canonical Structure GRing.Ring.zmodType.
Canonical Structure GRing.UnitRing.eqType.
Canonical Structure GRing.UnitRing.choiceType.
Canonical Structure GRing.UnitRing.zmodType.
Canonical Structure GRing.UnitRing.ringType.
Canonical Structure GRing.ComRing.eqType.
Canonical Structure GRing.ComRing.choiceType.
Canonical Structure GRing.ComRing.zmodType.
Canonical Structure GRing.ComRing.ringType.
Canonical Structure GRing.ComUnitRing.eqType.
Canonical Structure GRing.ComUnitRing.choiceType.
Canonical Structure GRing.ComUnitRing.zmodType.
Canonical Structure GRing.ComUnitRing.ringType.
Canonical Structure GRing.ComUnitRing.unitRingType.
Canonical Structure GRing.ComUnitRing.comRingType.
Canonical Structure GRing.ComUnitRing.com_unitRingType.
Canonical Structure GRing.IntegralDomain.eqType.
Canonical Structure GRing.IntegralDomain.choiceType.
Canonical Structure GRing.IntegralDomain.zmodType.
Canonical Structure GRing.IntegralDomain.ringType.
Canonical Structure GRing.IntegralDomain.unitRingType.
Canonical Structure GRing.IntegralDomain.comRingType.
Canonical Structure GRing.IntegralDomain.comUnitRingType.
Canonical Structure GRing.Field.eqType.
Canonical Structure GRing.Field.choiceType.
Canonical Structure GRing.Field.zmodType.
Canonical Structure GRing.Field.ringType.
Canonical Structure GRing.Field.unitRingType.
Canonical Structure GRing.Field.comRingType.
Canonical Structure GRing.Field.comUnitRingType.
Canonical Structure GRing.Field.idomainType.
Canonical Structure GRing.DecidableField.eqType.
Canonical Structure GRing.DecidableField.choiceType.
Canonical Structure GRing.DecidableField.zmodType.
Canonical Structure GRing.DecidableField.ringType.
Canonical Structure GRing.DecidableField.unitRingType.
Canonical Structure GRing.DecidableField.comRingType.
Canonical Structure GRing.DecidableField.comUnitRingType.
Canonical Structure GRing.DecidableField.idomainType.
Canonical Structure GRing.DecidableField.fieldType.
Canonical Structure GRing.ClosedField.eqType.
Canonical Structure GRing.ClosedField.choiceType.
Canonical Structure GRing.ClosedField.zmodType.
Canonical Structure GRing.ClosedField.ringType.
Canonical Structure GRing.ClosedField.unitRingType.
Canonical Structure GRing.ClosedField.comRingType.
Canonical Structure GRing.ClosedField.comUnitRingType.
Canonical Structure GRing.ClosedField.idomainType.
Canonical Structure GRing.ClosedField.fieldType.
Canonical Structure GRing.ClosedField.decFieldType.

Canonical Structure GRing.add_monoid.
Canonical Structure GRing.add_comoid.
Canonical Structure GRing.mul_monoid.
Canonical Structure GRing.mul_comoid.
Canonical Structure GRing.muloid.
Canonical Structure GRing.addoid.

Canonical Structure GRing.Lmodule.eqType.
Canonical Structure GRing.Lmodule.choiceType.
Canonical Structure GRing.Lmodule.zmodType.

Canonical Structure GRing.NCalgebra.eqType.
Canonical Structure GRing.NCalgebra.choiceType.
Canonical Structure GRing.NCalgebra.zmodType.
Canonical Structure GRing.NCalgebra.ringType.
Canonical Structure GRing.NCalgebra.lmoduleType.


Notation "0" := (GRing.zero _) : ring_scope.
Notation "-%R" := (@GRing.opp _) : ring_scope.
Notation "- x" := (GRing.opp x) : ring_scope.
Notation "+%R" := (@GRing.add _).
Notation "x + y" := (GRing.add x y) : ring_scope.
Notation "x - y" := (GRing.add x (- y)) : ring_scope.
Notation "x *+ n" := (GRing.natmul x n) : ring_scope.
Notation "x *- n" := (GRing.natmul (- x) n) : ring_scope.
Notation "s `_ i" := (seq.nth 0%R s%R i) : ring_scope.

Notation "1" := (GRing.one _) : ring_scope.
Notation "- 1" := (- (1))%R : ring_scope.

Notation "n %:R" := (GRing.natmul 1 n) : ring_scope.
Notation "[ 'char' R ]" := (GRing.char (Phant R)) : ring_scope.
Notation Frobenius_aut chRp := (GRing.Frobenius_aut chRp).
Notation "*%R" := (@GRing.mul _).
Notation "x * y" := (GRing.mul x y) : ring_scope.
Notation "x ^+ n" := (GRing.exp x n) : ring_scope.
Notation "x ^-1" := (GRing.inv x) : ring_scope.
Notation "x ^- n" := (x ^+ n)^-1%R : ring_scope.
Notation "x / y" := (GRing.mul x y^-1) : ring_scope.

Implicit Arguments GRing.unitDef [].


Notation "''X_' i" := (GRing.Var _ i) : term_scope.
Notation "n %:R" := (GRing.NatConst _ n) : term_scope.
Notation "0" := 0%:R%T : term_scope.
Notation "1" := 1%:R%T : term_scope.
Notation "x %:T" := (GRing.Const x) : term_scope.
Infix "+" := GRing.Add : term_scope.
Notation "- t" := (GRing.Opp t) : term_scope.
Notation "t - u" := (GRing.Add t (- u)) : term_scope.
Infix "*" := GRing.Mul : term_scope.
Infix "*+" := GRing.NatMul : term_scope.
Notation "t ^-1" := (GRing.Inv t) : term_scope.
Notation "t / u" := (GRing.Mul t u^-1) : term_scope.
Infix "^+" := GRing.Exp : term_scope.
Infix "==" := GRing.Equal : term_scope.
Notation "x != y" := (GRing.Not (x == y)) : term_scope.
Infix "/\" := GRing.And : term_scope.
Infix "\/" := GRing.Or : term_scope.
Infix "==>" := GRing.Implies : term_scope.
Notation "~ f" := (GRing.Not f) : term_scope.
Notation "''exists' ''X_' i , f" := (GRing.Exists i f) : term_scope.
Notation "''forall' ''X_' i , f" := (GRing.Forall i f) : term_scope.

Notation "*:%R" := (@GRing.scale _ _) : ring_scope.
Notation "a *: m" := (GRing.scale a m) (at level 40) : ring_scope.

Notation "\sum_ ( <- r | P ) F" :=
  (\big[+%R/0%R]_(<- r | P%B) F%R) : ring_scope.
Notation "\sum_ ( i <- r | P ) F" :=
  (\big[+%R/0%R]_(i <- r | P%B) F%R) : ring_scope.
Notation "\sum_ ( i <- r ) F" :=
  (\big[+%R/0%R]_(i <- r) F%R) : ring_scope.
Notation "\sum_ ( m <= i < n | P ) F" :=
  (\big[+%R/0%R]_(m <= i < n | P%B) F%R) : ring_scope.
Notation "\sum_ ( m <= i < n ) F" :=
  (\big[+%R/0%R]_(m <= i < n) F%R) : ring_scope.
Notation "\sum_ ( i | P ) F" :=
  (\big[+%R/0%R]_(i | P%B) F%R) : ring_scope.
Notation "\sum_ i F" :=
  (\big[+%R/0%R]_i F%R) : ring_scope.
Notation "\sum_ ( i : t | P ) F" :=
  (\big[+%R/0%R]_(i : t | P%B) F%R) (only parsing) : ring_scope.
Notation "\sum_ ( i : t ) F" :=
  (\big[+%R/0%R]_(i : t) F%R) (only parsing) : ring_scope.
Notation "\sum_ ( i < n | P ) F" :=
  (\big[+%R/0%R]_(i < n | P%B) F%R) : ring_scope.
Notation "\sum_ ( i < n ) F" :=
  (\big[+%R/0%R]_(i < n) F%R) : ring_scope.
Notation "\sum_ ( i \in A | P ) F" :=
  (\big[+%R/0%R]_(i \in A | P%B) F%R) : ring_scope.
Notation "\sum_ ( i \in A ) F" :=
  (\big[+%R/0%R]_(i \in A) F%R) : ring_scope.

Notation "\prod_ ( <- r | P ) F" :=
  (\big[*%R/1%R]_(<- r | P%B) F%R) : ring_scope.
Notation "\prod_ ( i <- r | P ) F" :=
  (\big[*%R/1%R]_(i <- r | P%B) F%R) : ring_scope.
Notation "\prod_ ( i <- r ) F" :=
  (\big[*%R/1%R]_(i <- r) F%R) : ring_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
  (\big[*%R/1%R]_(m <= i < n | P%B) F%R) : ring_scope.
Notation "\prod_ ( m <= i < n ) F" :=
  (\big[*%R/1%R]_(m <= i < n) F%R) : ring_scope.
Notation "\prod_ ( i | P ) F" :=
  (\big[*%R/1%R]_(i | P%B) F%R) : ring_scope.
Notation "\prod_ i F" :=
  (\big[*%R/1%R]_i F%R) : ring_scope.
Notation "\prod_ ( i : t | P ) F" :=
  (\big[*%R/1%R]_(i : t | P%B) F%R) (only parsing) : ring_scope.
Notation "\prod_ ( i : t ) F" :=
  (\big[*%R/1%R]_(i : t) F%R) (only parsing) : ring_scope.
Notation "\prod_ ( i < n | P ) F" :=
  (\big[*%R/1%R]_(i < n | P%B) F%R) : ring_scope.
Notation "\prod_ ( i < n ) F" :=
  (\big[*%R/1%R]_(i < n) F%R) : ring_scope.
Notation "\prod_ ( i \in A | P ) F" :=
  (\big[*%R/1%R]_(i \in A | P%B) F%R) : ring_scope.
Notation "\prod_ ( i \in A ) F" :=
  (\big[*%R/1%R]_(i \in A) F%R) : ring_scope.

Notation zmodType := GRing.Zmodule.type.
Notation ZmodType T m := (@GRing.Zmodule.pack T m _ _ id).
Notation ZmodMixin := GRing.Zmodule.Mixin.
Notation "[ 'zmodType' 'of' T 'for' cT ]" := (@GRing.Zmodule.clone T cT _ idfun)
  (at level 0, format "[ 'zmodType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'zmodType' 'of' T ]" := (@GRing.Zmodule.clone T _ _ id)
  (at level 0, format "[ 'zmodType' 'of' T ]") : form_scope.

Notation ringType := GRing.Ring.type.
Notation RingType T m := (@GRing.Ring.pack T _ m _ _ id _ id).
Notation RingMixin := GRing.Ring.Mixin.
Notation RevRingType := GRing.RevRingType.
Notation "[ 'ringType' 'of' T 'for' cT ]" := (@GRing.Ring.clone T cT _ idfun)
  (at level 0, format "[ 'ringType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'ringType' 'of' T ]" := (@GRing.Ring.clone T _ _ id)
  (at level 0, format "[ 'ringType' 'of' T ]") : form_scope.

Notation comRingType := GRing.ComRing.type.
Notation ComRingType T m := (@GRing.ComRing.pack T _ m _ _ id _ id).
Notation ComRingMixin := GRing.ComRing.RingMixin.
Notation "[ 'comRingType' 'of' T 'for' cT ]" :=
    (@GRing.ComRing.clone T cT _ idfun)
  (at level 0, format "[ 'comRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'comRingType' 'of' T ]" := (@GRing.ComRing.clone T _ _ id)
  (at level 0, format "[ 'comRingType' 'of' T ]") : form_scope.

Notation unitRingType := GRing.UnitRing.type.
Notation UnitRingType T m := (@GRing.UnitRing.pack T _ m _ _ id _ id).
Notation UnitRingMixin := GRing.UnitRing.EtaMixin.
Notation "[ 'unitRingType' 'of' T 'for' cT ]" :=
    (@GRing.UnitRing.clone T cT _ idfun)
  (at level 0, format "[ 'unitRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'unitRingType' 'of' T ]" := (@GRing.UnitRing.clone T _ _ id)
  (at level 0, format "[ 'unitRingType' 'of' T ]") : form_scope.

Notation comUnitRingType := GRing.ComUnitRing.type.
Notation ComUnitRingMixin := GRing.ComUnitRing.Mixin.
Notation "[ 'comUnitRingType' 'of' T ]" :=
    (@GRing.ComUnitRing.pack T _ _ id _ _ id)
  (at level 0, format "[ 'comUnitRingType' 'of' T ]") : form_scope.

Notation idomainType := GRing.IntegralDomain.type.
Notation IdomainType T m := (@GRing.IntegralDomain.pack T _ m _ _ id _ id).
Notation "[ 'idomainType' 'of' T 'for' cT ]" :=
    (@GRing.IntegralDomain.clone T cT _ idfun)
  (at level 0, format "[ 'idomainType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'idomainType' 'of' T ]" := (@GRing.IntegralDomain.clone T _ _ id)
  (at level 0, format "[ 'idomainType' 'of' T ]") : form_scope.

Notation fieldType := GRing.Field.type.
Notation FieldType T m := (@GRing.Field.pack T _ m _ _ id _ id).
Notation FieldUnitMixin := GRing.Field.UnitMixin.
Notation FieldIdomainMixin := GRing.Field.IdomainMixin.
Notation FieldMixin := GRing.Field.Mixin.
Notation "[ 'fieldType' 'of' T 'for' cT ]" := (@GRing.Field.clone T cT _ idfun)
  (at level 0, format "[ 'fieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'fieldType' 'of' T ]" := (@GRing.Field.clone T _ _ id)
  (at level 0, format "[ 'fieldType' 'of' T ]") : form_scope.

Notation decFieldType := GRing.DecidableField.type.
Notation DecFieldType T m := (@GRing.DecidableField.pack T _ m _ _ id _ id).
Notation DecFieldMixin := GRing.DecidableField.Mixin.
Notation "[ 'decFieldType' 'of' T 'for' cT ]" :=
    (@GRing.DecidableField.clone T cT _ idfun)
  (at level 0, format "[ 'decFieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'decFieldType' 'of' T ]" := (@GRing.DecidableField.clone T _ _ id)
  (at level 0, format "[ 'decFieldType' 'of' T ]") : form_scope.

Notation closedFieldType := GRing.ClosedField.type.
Notation ClosedFieldType T m := (GRing.ClosedField.pack T _ m _ _ id _ id).
Notation "[ 'closedFieldType' 'of' T 'for' cT ]" :=
    (@GRing.ClosedField.clone T cT _ idfun)
  (at level 0,
   format "[ 'closedFieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'closedFieldType' 'of' T ]" := (@GRing.ClosedField.clone T _ _ id)
  (at level 0, format "[ 'closedFieldType' 'of' T ]") : form_scope.

Notation lmodType R := (GRing.Lmodule.type (Phant R)).
Notation LmodType R T m :=
   (@GRing.Lmodule.pack _ (Phant R) T _ m _ _ id _ id).
Notation LmodMixin := GRing.Lmodule.Mixin.
Notation "[ 'lmodType' [ R ] 'of' T 'for' cT ]" :=
  (@GRing.Lmodule.clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'lmodType' [ R ] 'of' T 'for' cT ]")
  : form_scope.
Notation "[ 'lmodType' [ R ] 'of' T ]" :=
  (@GRing.Lmodule.clone _ (Phant R) T _ _ id)
  (at level 0, format "[ 'lmodType' [ R ] 'of' T ]") : form_scope.

Notation ncalgebraType R := (GRing.NCalgebra.type (Phant R)).
Notation NCalgebraType R T m a :=
   (@GRing.NCalgebra.pack _ (Phant R) T _ m a _ _ id _ _ id _ id).
Notation "[ 'ncalgebraType' [ R ] 'of' T 'for' cT ]" :=
  (@GRing.NCalgebra.clone _ (Phant R) T cT _ idfun)
  (at level 0, format "[ 'ncalgebraType' [ R ] 'of' T 'for' cT ]")
  : form_scope.
Notation "[ 'ncalgebraType' [ R ] 'of' T ]" :=
  (@GRing.NCalgebra.clone _ (Phant R) T _ _ id)
  (at level 0, format "[ 'ncalgebraType' [ R ] 'of' T ]") : form_scope.