Library mathcomp.algebra.ssrnum

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

Require Import mathcomp.ssreflect.ssreflect.

This file defines some classes to manipulate number structures, i.e structures with an order and a norm

NumDomain (Integral domain with an order and a norm)

NumMixin == the mixin that provides an order and a norm over a ring and their characteristic properties. numDomainType == interface for a num integral domain. NumDomainType T m == packs the num mixin into a numberDomainType. The carrier T must have a integral domain structure. [numDomainType of T for S ] == T-clone of the numDomainType structure S. [numDomainType of T] == clone of a canonical numDomainType structure on T.

NumField (Field with an order and a norm)

numFieldType == interface for a num field. [numFieldType of T] == clone of a canonical numFieldType structure on T

NumClosedField (Closed Field with an order and a norm)

numClosedFieldType == interface for a num closed field. [numClosedFieldType of T] == clone of a canonical numClosedFieldType structure on T

RealDomain (Num domain where all elements are positive or negative)

realDomainType == interface for a real integral domain. RealDomainType T r == packs the real axiom r into a realDomainType. The carrier T must have a num domain structure. [realDomainType of T for S ] == T-clone of the realDomainType structure S. [realDomainType of T] == clone of a canonical realDomainType structure on T.

RealField (Num Field where all elements are positive or negative)

realFieldType == interface for a real field. [realFieldType of T] == clone of a canonical realFieldType structure on T

ArchiField (A Real Field with the archimedean axiom)

archiFieldType == interface for an archimedean field. ArchiFieldType T r == packs the archimeadean axiom r into an archiFieldType. The carrier T must have a real field type structure. [archiFieldType of T for S ] == T-clone of the archiFieldType structure S. [archiFieldType of T] == clone of a canonical archiFieldType structure on T

RealClosedField (Real Field with the real closed axiom)

realClosedFieldType == interface for a real closed field. RealClosedFieldType T r == packs the real closed axiom r into a realClodedFieldType. The carrier T must have a real field type structure. [realClosedFieldType of T for S ] == T-clone of the realClosedFieldType structure S. [realClosedFieldype of T] == clone of a canonical realClosedFieldType structure on T.
Over these structures, we have the following operations `|x| == norm of x. x <= y <=> x is less than or equal to y (:= '|y - x| == y - x). x < y <=> x is less than y (:= (x <= y) && (x != y)). x <= y ?= iff C <-> x is less than y, or equal iff C is true. Num.sg x == sign of x: equal to 0 iff x = 0, to 1 iff x > 0, and to -1 in all other cases (including x < 0). x \is a Num.pos <=> x is positive (:= x > 0). x \is a Num.neg <=> x is negative (:= x < 0). x \is a Num.nneg <=> x is positive or 0 (:= x >= 0). x \is a Num.real <=> x is real (:= x >= 0 or x < 0). Num.min x y == minimum of x y Num.max x y == maximum of x y Num.bound x == in archimedean fields, and upper bound for x, i.e., and n such that `|x| < n%:R. Num.sqrt x == in a real-closed field, a positive square root of x if x >= 0, or 0 otherwise.
There are now three distinct uses of the symbols <, <=, > and >=: 0-ary, unary (prefix) and binary (infix). 0. <%R, <=%R, >%R, >=%R stand respectively for lt, le, gt and ge. 1. (< x), (<= x), (> x), (>= x) stand respectively for (gt x), (ge x), (lt x), (le x). So (< x) is a predicate characterizing elements smaller than x. 2. (x < y), (x <= y), ... mean what they are expected to. These convention are compatible with haskell's, where ((< y) x) = (x < y) = ((<) x y), except that we write <%R instead of (<).
  • list of prefixes : p : positive n : negative sp : strictly positive sn : strictly negative i : interior = in [0, 1] or ]0, 1[ e : exterior = in [1, +oo[ or ]1; +oo[ w : non strict (weak) monotony

Set Implicit Arguments.

Local Open Scope ring_scope.
Import GRing.Theory.

Reserved Notation "<= y" (at level 35).
Reserved Notation ">= y" (at level 35).
Reserved Notation "< y" (at level 35).
Reserved Notation "> y" (at level 35).
Reserved Notation "<= y :> T" (at level 35, y at next level).
Reserved Notation ">= y :> T" (at level 35, y at next level).
Reserved Notation "< y :> T" (at level 35, y at next level).
Reserved Notation "> y :> T" (at level 35, y at next level).

Module Num.

Principal mixin; further classes add axioms rather than operations.
Record mixin_of (R : ringType) := Mixin {
  norm_op : R R;
  le_op : rel R;
  lt_op : rel R;
  _ : x y, le_op (norm_op (x + y)) (norm_op x + norm_op y);
  _ : x y, lt_op 0 x lt_op 0 y lt_op 0 (x + y);
  _ : x, norm_op x = 0 x = 0;
  _ : x y, le_op 0 x le_op 0 y le_op x y || le_op y x;
  _ : {morph norm_op : x y / x × y};
  _ : x y, (le_op x y) = (norm_op (y - x) == y - x);
  _ : x y, (lt_op x y) = (y != x) && (le_op x y)
}.


Base interface.
Module NumDomain.

Section ClassDef.

Record class_of T := Class {
  base : GRing.IntegralDomain.class_of T;
  mixin : mixin_of (ring_for T base)
}.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (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 clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (ring_for T b0)) :=
  fun bT b & phant_id (GRing.IntegralDomain.class bT) b
  fun m & phant_id m0 mPack (@Class T b m) T.

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Notation numDomainType := type.
Notation NumMixin := Mixin.
Notation NumDomainType T m := (@pack T _ m _ _ id _ id).
Notation "[ 'numDomainType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'numDomainType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'numDomainType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'numDomainType' 'of' T ]") : form_scope.
End Exports.

End NumDomain.
Import NumDomain.Exports.

Module Import Def. Section Def.
Import NumDomain.
Context {R : type}.
Implicit Types (x y : R) (C : bool).

Definition normr : R R := norm_op (class R).
Definition ler : rel R := le_op (class R).
Definition ltr : rel R := lt_op (class R).

Definition ger : simpl_rel R := [rel x y | y x].
Definition gtr : simpl_rel R := [rel x y | y < x].
Definition lerif x y C : Prop := ((x y) × ((x == y) = C))%type.
Definition sgr x : R := if x == 0 then 0 else if x < 0 then -1 else 1.
Definition minr x y : R := if x y then x else y.
Definition maxr x y : R := if y x then x else y.

Definition Rpos : qualifier 0 R := [qualify x : R | 0 < x].
Definition Rneg : qualifier 0 R := [qualify x : R | x < 0].
Definition Rnneg : qualifier 0 R := [qualify x : R | 0 x].
Definition Rreal : qualifier 0 R := [qualify x : R | (0 x) || (x 0)].
End Def. End Def.

Shorter qualified names, when Num.Def is not imported.
Notation norm := normr.
Notation le := ler.
Notation lt := ltr.
Notation ge := ger.
Notation gt := gtr.
Notation sg := sgr.
Notation max := maxr.
Notation min := minr.
Notation pos := Rpos.
Notation neg := Rneg.
Notation nneg := Rnneg.
Notation real := Rreal.

Module Keys. Section Keys.
Variable R : numDomainType.
Fact Rpos_key : pred_key (@pos R).
Definition Rpos_keyed := KeyedQualifier Rpos_key.
Fact Rneg_key : pred_key (@real R).
Definition Rneg_keyed := KeyedQualifier Rneg_key.
Fact Rnneg_key : pred_key (@nneg R).
Definition Rnneg_keyed := KeyedQualifier Rnneg_key.
Fact Rreal_key : pred_key (@real R).
Definition Rreal_keyed := KeyedQualifier Rreal_key.
Definition ler_of_leif x y C (le_xy : @lerif R x y C) := le_xy.1 : le x y.
End Keys. End Keys.

(Exported) symbolic syntax.
Module Import Syntax.
Import Def Keys.

Notation "`| x |" := (norm x) : ring_scope.

Notation "<%R" := lt : ring_scope.
Notation ">%R" := gt : ring_scope.
Notation "<=%R" := le : ring_scope.
Notation ">=%R" := ge : ring_scope.
Notation "<?=%R" := lerif : ring_scope.

Notation "< y" := (gt y) : ring_scope.
Notation "< y :> T" := (< (y : T)) : ring_scope.
Notation "> y" := (lt y) : ring_scope.
Notation "> y :> T" := (> (y : T)) : ring_scope.

Notation "<= y" := (ge y) : ring_scope.
Notation "<= y :> T" := ( (y : T)) : ring_scope.
Notation ">= y" := (le y) : ring_scope.
Notation ">= y :> T" := ( (y : T)) : ring_scope.

Notation "x < y" := (lt x y) : ring_scope.
Notation "x < y :> T" := ((x : T) < (y : T)) : ring_scope.
Notation "x > y" := (y < x) (only parsing) : ring_scope.
Notation "x > y :> T" := ((x : T) > (y : T)) (only parsing) : ring_scope.

Notation "x <= y" := (le x y) : ring_scope.
Notation "x <= y :> T" := ((x : T) (y : T)) : ring_scope.
Notation "x >= y" := (y x) (only parsing) : ring_scope.
Notation "x >= y :> T" := ((x : T) (y : T)) (only parsing) : ring_scope.

Notation "x <= y <= z" := ((x y) && (y z)) : ring_scope.
Notation "x < y <= z" := ((x < y) && (y z)) : ring_scope.
Notation "x <= y < z" := ((x y) && (y < z)) : ring_scope.
Notation "x < y < z" := ((x < y) && (y < z)) : ring_scope.

Notation "x <= y ?= 'iff' C" := (lerif x y C) : ring_scope.
Notation "x <= y ?= 'iff' C :> R" := ((x : R) (y : R) ?= iff C)
  (only parsing) : ring_scope.

Coercion ler_of_leif : lerif >-> is_true.

Canonical Rpos_keyed.
Canonical Rneg_keyed.
Canonical Rnneg_keyed.
Canonical Rreal_keyed.

End Syntax.

Section ExtensionAxioms.

Variable R : numDomainType.

Definition real_axiom : Prop := x : R, x \is real.

Definition archimedean_axiom : Prop := x : R, ub, `|x| < ub%:R.

Definition real_closed_axiom : Prop :=
   (p : {poly R}) (a b : R),
    a b p.[a] 0 p.[b] exists2 x, a x b & root p x.

End ExtensionAxioms.


The rest of the numbers interface hierarchy.
Module NumField.

Section ClassDef.

Record class_of R :=
  Class { base : GRing.Field.class_of R; mixin : mixin_of (ring_for R base) }.
Definition base2 R (c : class_of R) := NumDomain.Class (mixin c).

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (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 pack :=
  fun bT b & phant_id (GRing.Field.class bT) (b : GRing.Field.class_of T) ⇒
  fun mT m & phant_id (NumDomain.class mT) (@NumDomain.Class T b m) ⇒
  Pack (@Class T b m) T.

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition numDomainType := @NumDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.
Definition join_numDomainType := @NumDomain.Pack fieldType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.Field.class_of.
Coercion base2 : class_of >-> NumDomain.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Notation numFieldType := type.
Notation "[ 'numFieldType' 'of' T ]" := (@pack T _ _ id _ _ id)
  (at level 0, format "[ 'numFieldType' 'of' T ]") : form_scope.
End Exports.

End NumField.
Import NumField.Exports.

Module ClosedField.

Section ClassDef.

Record class_of R := Class {
  base : GRing.ClosedField.class_of R;
  mixin : mixin_of (ring_for R base)
}.
Definition base2 R (c : class_of R) := NumField.Class (mixin c).

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (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 pack :=
  fun bT b & phant_id (GRing.ClosedField.class bT)
                      (b : GRing.ClosedField.class_of T) ⇒
  fun mT m & phant_id (NumField.class mT) (@NumField.Class T b m) ⇒
  Pack (@Class T b m) T.

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition numDomainType := @NumDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.
Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT.
Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT.
Definition join_dec_numDomainType := @NumDomain.Pack decFieldType xclass xT.
Definition join_dec_numFieldType := @NumField.Pack decFieldType xclass xT.
Definition join_numDomainType := @NumDomain.Pack closedFieldType xclass xT.
Definition join_numFieldType := @NumField.Pack closedFieldType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.ClosedField.class_of.
Coercion base2 : class_of >-> NumField.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion decFieldType : type >-> GRing.DecidableField.type.
Canonical decFieldType.
Coercion closedFieldType : type >-> GRing.ClosedField.type.
Canonical closedFieldType.
Canonical join_dec_numDomainType.
Canonical join_dec_numFieldType.
Canonical join_numDomainType.
Canonical join_numFieldType.
Notation numClosedFieldType := type.
Notation "[ 'numClosedFieldType' 'of' T ]" := (@pack T _ _ id _ _ id)
  (at level 0, format "[ 'numClosedFieldType' 'of' T ]") : form_scope.
End Exports.

End ClosedField.
Import ClosedField.Exports.

Module RealDomain.

Section ClassDef.

Record class_of R :=
  Class {base : NumDomain.class_of R; _ : @real_axiom (num_for R base)}.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (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 clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : real_axiom (num_for T b0)) :=
  fun bT b & phant_id (NumDomain.class bT) b
  fun m & phant_id m0 mPack (@Class T b m) T.

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition numDomainType := @NumDomain.Pack cT xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> NumDomain.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Notation realDomainType := type.
Notation RealDomainType T m := (@pack T _ m _ _ id _ id).
Notation "[ 'realDomainType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'realDomainType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'realDomainType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'realDomainType' 'of' T ]") : form_scope.
End Exports.

End RealDomain.
Import RealDomain.Exports.

Module RealField.

Section ClassDef.

Record class_of R :=
  Class { base : NumField.class_of R; mixin : real_axiom (num_for R base) }.
Definition base2 R (c : class_of R) := RealDomain.Class (@mixin R c).

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (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 pack :=
  fun bT b & phant_id (NumField.class bT) (b : NumField.class_of T) ⇒
  fun mT m & phant_id (RealDomain.class mT) (@RealDomain.Class T b m) ⇒
  Pack (@Class T b m) T.

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition numDomainType := @NumDomain.Pack cT xclass xT.
Definition realDomainType := @RealDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.
Definition numFieldType := @NumField.Pack cT xclass xT.
Definition join_realDomainType := @RealDomain.Pack numFieldType xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> NumField.class_of.
Coercion base2 : class_of >-> RealDomain.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Coercion realDomainType : type >-> RealDomain.type.
Canonical realDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion numFieldType : type >-> NumField.type.
Canonical numFieldType.
Canonical join_realDomainType.
Notation realFieldType := type.
Notation "[ 'realFieldType' 'of' T ]" := (@pack T _ _ id _ _ id)
  (at level 0, format "[ 'realFieldType' 'of' T ]") : form_scope.
End Exports.

End RealField.
Import RealField.Exports.

Module ArchimedeanField.

Section ClassDef.

Record class_of R :=
  Class { base : RealField.class_of R; _ : archimedean_axiom (num_for R base) }.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (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 clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : archimedean_axiom (num_for T b0)) :=
  fun bT b & phant_id (RealField.class bT) b
  fun m & phant_id m0 mPack (@Class T b m) T.

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition numDomainType := @NumDomain.Pack cT xclass xT.
Definition realDomainType := @RealDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.
Definition numFieldType := @NumField.Pack cT xclass xT.
Definition realFieldType := @RealField.Pack cT xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> RealField.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Coercion realDomainType : type >-> RealDomain.type.
Canonical realDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion numFieldType : type >-> NumField.type.
Canonical numFieldType.
Coercion realFieldType : type >-> RealField.type.
Canonical realFieldType.
Notation archiFieldType := type.
Notation ArchiFieldType T m := (@pack T _ m _ _ id _ id).
Notation "[ 'archiFieldType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'archiFieldType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'archiFieldType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'archiFieldType' 'of' T ]") : form_scope.
End Exports.

End ArchimedeanField.
Import ArchimedeanField.Exports.

Module RealClosedField.

Section ClassDef.

Record class_of R :=
  Class { base : RealField.class_of R; _ : real_closed_axiom (num_for R base) }.

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (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 clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : real_closed_axiom (num_for T b0)) :=
  fun bT b & phant_id (RealField.class bT) b
  fun m & phant_id m0 mPack (@Class T b m) T.

Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @GRing.Zmodule.Pack cT xclass xT.
Definition ringType := @GRing.Ring.Pack cT xclass xT.
Definition comRingType := @GRing.ComRing.Pack cT xclass xT.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT.
Definition numDomainType := @NumDomain.Pack cT xclass xT.
Definition realDomainType := @RealDomain.Pack cT xclass xT.
Definition fieldType := @GRing.Field.Pack cT xclass xT.
Definition numFieldType := @NumField.Pack cT xclass xT.
Definition realFieldType := @RealField.Pack cT xclass xT.

End ClassDef.

Module Exports.
Coercion base : class_of >-> RealField.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Coercion realDomainType : type >-> RealDomain.type.
Canonical realDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion numFieldType : type >-> NumField.type.
Canonical numFieldType.
Coercion realFieldType : type >-> RealField.type.
Canonical realFieldType.
Notation rcfType := Num.RealClosedField.type.
Notation RcfType T m := (@pack T _ m _ _ id _ id).
Notation "[ 'rcfType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'rcfType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'rcfType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'rcfType' 'of' T ]") : form_scope.
End Exports.

End RealClosedField.
Import RealClosedField.Exports.

The elementary theory needed to support the definition of the derived operations for the extensions described above.
Module Import Internals.

Section Domain.
Variable R : numDomainType.
Implicit Types x y : R.

Lemmas from the signature

Lemma normr0_eq0 x : `|x| = 0 x = 0.

Lemma ler_norm_add x y : `|x + y| `|x| + `|y|.

Lemma addr_gt0 x y : 0 < x 0 < y 0 < x + y.

Lemma ger_leVge x y : 0 x 0 y (x y) || (y x).

Lemma normrM : {morph norm : x y / x × y : R}.

Lemma ler_def x y : (x y) = (`|y - x| == y - x).

Lemma ltr_def x y : (x < y) = (y != x) && (x y).

Basic consequences (just enough to get predicate closure properties).

Lemma ger0_def x : (0 x) = (`|x| == x).

Lemma subr_ge0 x y : (0 x - y) = (y x).

Lemma oppr_ge0 x : (0 - x) = (x 0).

Lemma ler01 : 0 1 :> R.

Lemma ltr01 : 0 < 1 :> R.

Lemma ltrW x y : x < y x y.

Lemma lerr x : x x.

Lemma le0r x : (0 x) = (x == 0) || (0 < x).

Lemma addr_ge0 x y : 0 x 0 y 0 x + y.

Lemma pmulr_rgt0 x y : 0 < x (0 < x × y) = (0 < y).

Closure properties of the real predicates.

Lemma posrE x : (x \is pos) = (0 < x).
Lemma nnegrE x : (x \is nneg) = (0 x).
Lemma realE x : (x \is real) = (0 x) || (x 0).

Fact pos_divr_closed : divr_closed (@pos R).
Canonical pos_mulrPred := MulrPred pos_divr_closed.
Canonical pos_divrPred := DivrPred pos_divr_closed.

Fact nneg_divr_closed : divr_closed (@nneg R).
Canonical nneg_mulrPred := MulrPred nneg_divr_closed.
Canonical nneg_divrPred := DivrPred nneg_divr_closed.

Fact nneg_addr_closed : addr_closed (@nneg R).
Canonical nneg_addrPred := AddrPred nneg_addr_closed.
Canonical nneg_semiringPred := SemiringPred nneg_divr_closed.

Fact real_oppr_closed : oppr_closed (@real R).
Canonical real_opprPred := OpprPred real_oppr_closed.

Fact real_addr_closed : addr_closed (@real R).
Canonical real_addrPred := AddrPred real_addr_closed.
Canonical real_zmodPred := ZmodPred real_oppr_closed.

Fact real_divr_closed : divr_closed (@real R).
Canonical real_mulrPred := MulrPred real_divr_closed.
Canonical real_smulrPred := SmulrPred real_divr_closed.
Canonical real_divrPred := DivrPred real_divr_closed.
Canonical real_sdivrPred := SdivrPred real_divr_closed.
Canonical real_semiringPred := SemiringPred real_divr_closed.
Canonical real_subringPred := SubringPred real_divr_closed.
Canonical real_divringPred := DivringPred real_divr_closed.

End Domain.

Lemma num_real (R : realDomainType) (x : R) : x \is real.

Fact archi_bound_subproof (R : archiFieldType) : archimedean_axiom R.

Section RealClosed.
Variable R : rcfType.

Lemma poly_ivt : real_closed_axiom R.

Fact sqrtr_subproof (x : R) :
  exists2 y, 0 y & if 0 x return bool then y ^+ 2 == x else y == 0.

End RealClosed.

End Internals.

Module PredInstances.

Canonical pos_mulrPred.
Canonical pos_divrPred.

Canonical nneg_addrPred.
Canonical nneg_mulrPred.
Canonical nneg_divrPred.
Canonical nneg_semiringPred.

Canonical real_addrPred.
Canonical real_opprPred.
Canonical real_zmodPred.
Canonical real_mulrPred.
Canonical real_smulrPred.
Canonical real_divrPred.
Canonical real_sdivrPred.
Canonical real_semiringPred.
Canonical real_subringPred.
Canonical real_divringPred.

End PredInstances.

Module Import ExtraDef.

Definition archi_bound {R} x := sval (sigW (@archi_bound_subproof R x)).

Definition sqrtr {R} x := s2val (sig2W (@sqrtr_subproof R x)).

End ExtraDef.

Notation bound := archi_bound.
Notation sqrt := sqrtr.

Module Theory.

Section NumIntegralDomainTheory.

Variable R : numDomainType.
Implicit Types x y z t : R.

Lemmas from the signature (reexported from internals).

Definition ler_norm_add x y : `|x + y| `|x| + `|y| := ler_norm_add x y.
Definition addr_gt0 x y : 0 < x 0 < y 0 < x + y := @addr_gt0 R x y.
Definition normr0_eq0 x : `|x| = 0 x = 0 := @normr0_eq0 R x.
Definition ger_leVge x y : 0 x 0 y (x y) || (y x) :=
  @ger_leVge R x y.
Definition normrM : {morph normr : x y / x × y : R} := @normrM R.
Definition ler_def x y : (x y) = (`|y - x| == y - x) := @ler_def R x y.
Definition ltr_def x y : (x < y) = (y != x) && (x y) := @ltr_def R x y.

Predicate and relation definitions.

Lemma gerE x y : ge x y = (y x).
Lemma gtrE x y : gt x y = (y < x).
Lemma posrE x : (x \is pos) = (0 < x).
Lemma negrE x : (x \is neg) = (x < 0).
Lemma nnegrE x : (x \is nneg) = (0 x).
Lemma realE x : (x \is real) = (0 x) || (x 0).

General properties of <= and <

Lemma lerr x : x x.
Lemma ltrr x : x < x = false.
Lemma ltrW x y : x < y x y.
Hint Resolve lerr ltrr ltrW.

Lemma ltr_neqAle x y : (x < y) = (x != y) && (x y).

Lemma ler_eqVlt x y : (x y) = (x == y) || (x < y).

Lemma lt0r x : (0 < x) = (x != 0) && (0 x).
Lemma le0r x : (0 x) = (x == 0) || (0 < x).

Lemma lt0r_neq0 (x : R) : 0 < x x != 0.

Lemma ltr0_neq0 (x : R) : x < 0 x != 0.

Lemma gtr_eqF x y : y < x x == y = false.

Lemma ltr_eqF x y : x < y x == y = false.

Lemma pmulr_rgt0 x y : 0 < x (0 < x × y) = (0 < y).

Lemma pmulr_rge0 x y : 0 < x (0 x × y) = (0 y).

Integer comparisons and characteristic 0.
Lemma ler01 : 0 1 :> R.
Lemma ltr01 : 0 < 1 :> R.
Lemma ler0n n : 0 n%:R :> R.
Hint Resolve ler01 ltr01 ler0n.
Lemma ltr0Sn n : 0 < n.+1%:R :> R.
Lemma ltr0n n : (0 < n%:R :> R) = (0 < n)%N.
Hint Resolve ltr0Sn.

Lemma pnatr_eq0 n : (n%:R == 0 :> R) = (n == 0)%N.

Lemma char_num : [char R] =i pred0.

Properties of the norm.

Lemma ger0_def x : (0 x) = (`|x| == x).
Lemma normr_idP {x} : reflect (`|x| = x) (0 x).
Lemma ger0_norm x : 0 x `|x| = x.

Lemma normr0 : `|0| = 0 :> R.
Lemma normr1 : `|1| = 1 :> R.
Lemma normr_nat n : `|n%:R| = n%:R :> R.
Lemma normrMn x n : `|x *+ n| = `|x| *+ n.

Lemma normr_prod I r (P : pred I) (F : I R) :
  `|\prod_(i <- r | P i) F i| = \prod_(i <- r | P i) `|F i|.

Lemma normrX n x : `|x ^+ n| = `|x| ^+ n.

Lemma normr_unit : {homo (@norm R) : x / x \is a GRing.unit}.

Lemma normrV : {in GRing.unit, {morph (@normr R) : x / x ^-1}}.

Lemma normr0P {x} : reflect (`|x| = 0) (x == 0).

Definition normr_eq0 x := sameP (`|x| =P 0) normr0P.

Lemma normrN1 : `|-1| = 1 :> R.

Lemma normrN x : `|- x| = `|x|.

Lemma distrC x y : `|x - y| = `|y - x|.

Lemma ler0_def x : (x 0) = (`|x| == - x).

Lemma normr_id x : `|`|x| | = `|x|.

Lemma normr_ge0 x : 0 `|x|.
Hint Resolve normr_ge0.

Lemma ler0_norm x : x 0 `|x| = - x.

Definition gtr0_norm x (hx : 0 < x) := ger0_norm (ltrW hx).
Definition ltr0_norm x (hx : x < 0) := ler0_norm (ltrW hx).

Comparision to 0 of a difference

Lemma subr_ge0 x y : (0 y - x) = (x y).
Lemma subr_gt0 x y : (0 < y - x) = (x < y).
Lemma subr_le0 x y : (y - x 0) = (y x).
Lemma subr_lt0 x y : (y - x < 0) = (y < x).

Definition subr_lte0 := (subr_le0, subr_lt0).
Definition subr_gte0 := (subr_ge0, subr_gt0).
Definition subr_cp0 := (subr_lte0, subr_gte0).

Ordered ring properties.

Lemma ler_asym : antisymmetric (<=%R : rel R).

Lemma eqr_le x y : (x == y) = (x y x).

Lemma ltr_trans : transitive (@ltr R).

Lemma ler_lt_trans y x z : x y y < z x < z.

Lemma ltr_le_trans y x z : x < y y z x < z.

Lemma ler_trans : transitive (@ler R).

Definition lter01 := (ler01, ltr01).
Definition lterr := (lerr, ltrr).

Lemma addr_ge0 x y : 0 x 0 y 0 x + y.

Lemma lerifP x y C : reflect (x y ?= iff C) (if C then x == y else x < y).

Lemma ltr_asym x y : x < y < x = false.

Lemma ler_anti : antisymmetric (@ler R).

Lemma ltr_le_asym x y : x < y x = false.

Lemma ler_lt_asym x y : x y < x = false.

Definition lter_anti := (=^~ eqr_le, ltr_asym, ltr_le_asym, ler_lt_asym).

Lemma ltr_geF x y : x < y (y x = false).

Lemma ler_gtF x y : x y (y < x = false).

Definition ltr_gtF x y hxy := ler_gtF (@ltrW x y hxy).

Norm and order properties.

Lemma normr_le0 x : (`|x| 0) = (x == 0).

Lemma normr_lt0 x : `|x| < 0 = false.

Lemma normr_gt0 x : (`|x| > 0) = (x != 0).

Definition normrE x := (normr_id, normr0, normr1, normrN1, normr_ge0, normr_eq0,
  normr_lt0, normr_le0, normr_gt0, normrN).

End NumIntegralDomainTheory.

Implicit Arguments ler01 [R].
Implicit Arguments ltr01 [R].
Implicit Arguments normr_idP [R x].
Implicit Arguments normr0P [R x].
Implicit Arguments lerifP [R x y C].
Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0.

Section NumIntegralDomainMonotonyTheory.

Variables R R' : numDomainType.
Implicit Types m n p : nat.
Implicit Types x y z : R.
Implicit Types u v w : R'.

Section AcrossTypes.

Variable D D' : pred R.
Variable (f : R R').

Lemma ltrW_homo : {homo f : x y / x < y} {homo f : x y / x y}.

Lemma ltrW_nhomo : {homo f : x y /~ x < y} {homo f : x y /~ x y}.

Lemma homo_inj_lt :
  injective f {homo f : x y / x y} {homo f : x y / x < y}.

Lemma nhomo_inj_lt :
  injective f {homo f : x y /~ x y} {homo f : x y /~ x < y}.

Lemma mono_inj : {mono f : x y / x y} injective f.

Lemma nmono_inj : {mono f : x y /~ x y} injective f.

Lemma lerW_mono : {mono f : x y / x y} {mono f : x y / x < y}.

Lemma lerW_nmono : {mono f : x y /~ x y} {mono f : x y /~ x < y}.

Monotony in D D'
Lemma ltrW_homo_in :
  {in D & D', {homo f : x y / x < y}} {in D & D', {homo f : x y / x y}}.

Lemma ltrW_nhomo_in :
  {in D & D', {homo f : x y /~ x < y}} {in D & D', {homo f : x y /~ x y}}.

Lemma homo_inj_in_lt :
    {in D & D', injective f} {in D & D', {homo f : x y / x y}}
  {in D & D', {homo f : x y / x < y}}.

Lemma nhomo_inj_in_lt :
    {in D & D', injective f} {in D & D', {homo f : x y /~ x y}}
  {in D & D', {homo f : x y /~ x < y}}.

Lemma mono_inj_in : {in D &, {mono f : x y / x y}} {in D &, injective f}.

Lemma nmono_inj_in :
  {in D &, {mono f : x y /~ x y}} {in D &, injective f}.

Lemma lerW_mono_in :
  {in D &, {mono f : x y / x y}} {in D &, {mono f : x y / x < y}}.

Lemma lerW_nmono_in :
  {in D &, {mono f : x y /~ x y}} {in D &, {mono f : x y /~ x < y}}.

End AcrossTypes.

Section NatToR.

Variable (f : nat R).

Lemma ltn_ltrW_homo :
    {homo f : m n / (m < n)%N >-> m < n}
  {homo f : m n / (m n)%N >-> m n}.

Lemma ltn_ltrW_nhomo :
    {homo f : m n / (n < m)%N >-> m < n}
  {homo f : m n / (n m)%N >-> m n}.

Lemma homo_inj_ltn_lt :
    injective f {homo f : m n / (m n)%N >-> m n}
  {homo f : m n / (m < n)%N >-> m < n}.

Lemma nhomo_inj_ltn_lt :
    injective f {homo f : m n / (n m)%N >-> m n}
  {homo f : m n / (n < m)%N >-> m < n}.

Lemma leq_mono_inj : {mono f : m n / (m n)%N >-> m n} injective f.

Lemma leq_nmono_inj : {mono f : m n / (n m)%N >-> m n} injective f.

Lemma leq_lerW_mono :
    {mono f : m n / (m n)%N >-> m n}
  {mono f : m n / (m < n)%N >-> m < n}.

Lemma leq_lerW_nmono :
    {mono f : m n / (n m)%N >-> m n}
  {mono f : m n / (n < m)%N >-> m < n}.

Lemma homo_leq_mono :
    {homo f : m n / (m < n)%N >-> m < n}
   {mono f : m n / (m n)%N >-> m n}.

Lemma nhomo_leq_mono :
    {homo f : m n / (n < m)%N >-> m < n}
  {mono f : m n / (n m)%N >-> m n}.

End NatToR.

End NumIntegralDomainMonotonyTheory.

Section NumDomainOperationTheory.

Variable R : numDomainType.
Implicit Types x y z t : R.

Comparision and opposite.

Lemma ler_opp2 : {mono -%R : x y /~ x y :> R}.
Hint Resolve ler_opp2.
Lemma ltr_opp2 : {mono -%R : x y /~ x < y :> R}.
Hint Resolve ltr_opp2.
Definition lter_opp2 := (ler_opp2, ltr_opp2).

Lemma ler_oppr x y : (x - y) = (y - x).

Lemma ltr_oppr x y : (x < - y) = (y < - x).

Definition lter_oppr := (ler_oppr, ltr_oppr).

Lemma ler_oppl x y : (- x y) = (- y x).

Lemma ltr_oppl x y : (- x < y) = (- y < x).

Definition lter_oppl := (ler_oppl, ltr_oppl).

Lemma oppr_ge0 x : (0 - x) = (x 0).

Lemma oppr_gt0 x : (0 < - x) = (x < 0).

Definition oppr_gte0 := (oppr_ge0, oppr_gt0).

Lemma oppr_le0 x : (- x 0) = (0 x).

Lemma oppr_lt0 x : (- x < 0) = (0 < x).

Definition oppr_lte0 := (oppr_le0, oppr_lt0).
Definition oppr_cp0 := (oppr_gte0, oppr_lte0).
Definition lter_oppE := (oppr_cp0, lter_opp2).

Lemma ge0_cp x : 0 x (- x 0) × (- x x).

Lemma gt0_cp x : 0 < x
  (0 x) × (- x 0) × (- x x) × (- x < 0) × (- x < x).

Lemma le0_cp x : x 0 (0 - x) × (x - x).

Lemma lt0_cp x :
  x < 0 (x 0) × (0 - x) × (x - x) × (0 < - x) × (x < - x).

Properties of the real subset.

Lemma ger0_real x : 0 x x \is real.

Lemma ler0_real x : x 0 x \is real.

Lemma gtr0_real x : 0 < x x \is real.

Lemma ltr0_real x : x < 0 x \is real.

Lemma real0 : 0 \is @real R.
Hint Resolve real0.

Lemma real1 : 1 \is @real R.
Hint Resolve real1.

Lemma realn n : n%:R \is @real R.

Lemma ler_leVge x y : x 0 y 0 (x y) || (y x).

Lemma real_leVge x y : x \is real y \is real (x y) || (y x).

Lemma realB : {in real &, x y, x - y \is real}.

Lemma realN : {mono (@GRing.opp R) : x / x \is real}.

:TODO: add a rpredBC in ssralg
Lemma realBC x y : (x - y \is real) = (y - x \is real).

Lemma realD : {in real &, x y, x + y \is real}.

dichotomy and trichotomy

CoInductive ler_xor_gt (x y : R) : R R bool bool Set :=
  | LerNotGt of x y : ler_xor_gt x y (y - x) (y - x) true false
  | GtrNotLe of y < x : ler_xor_gt x y (x - y) (x - y) false true.

CoInductive ltr_xor_ge (x y : R) : R R bool bool Set :=
  | LtrNotGe of x < y : ltr_xor_ge x y (y - x) (y - x) false true
  | GerNotLt of y x : ltr_xor_ge x y (x - y) (x - y) true false.

CoInductive comparer x y : R R
  bool bool bool bool bool bool Set :=
  | ComparerLt of x < y : comparer x y (y - x) (y - x)
    false false true false true false
  | ComparerGt of x > y : comparer x y (x - y) (x - y)
    false false false true false true
  | ComparerEq of x = y : comparer x y 0 0
    true true true true false false.

Lemma real_lerP x y :
    x \is real y \is real
  ler_xor_gt x y `|x - y| `|y - x| (x y) (y < x).

Lemma real_ltrP x y :
    x \is real y \is real
  ltr_xor_ge x y `|x - y| `|y - x| (y x) (x < y).

Lemma real_ltrNge : {in real &, x y, (x < y) = ~~ (y x)}.

Lemma real_lerNgt : {in real &, x y, (x y) = ~~ (y < x)}.

Lemma real_ltrgtP x y :
    x \is real y \is real
  comparer x y `|x - y| `|y - x|
                (y == x) (x == y) (x y) (y x) (x < y) (x > y).

CoInductive ger0_xor_lt0 (x : R) : R bool bool Set :=
  | Ger0NotLt0 of 0 x : ger0_xor_lt0 x x false true
  | Ltr0NotGe0 of x < 0 : ger0_xor_lt0 x (- x) true false.

CoInductive ler0_xor_gt0 (x : R) : R bool bool Set :=
  | Ler0NotLe0 of x 0 : ler0_xor_gt0 x (- x) false true
  | Gtr0NotGt0 of 0 < x : ler0_xor_gt0 x x true false.

CoInductive comparer0 x :
               R bool bool bool bool bool bool Set :=
  | ComparerGt0 of 0 < x : comparer0 x x false false false true false true
  | ComparerLt0 of x < 0 : comparer0 x (- x) false false true false true false
  | ComparerEq0 of x = 0 : comparer0 x 0 true true true true false false.

Lemma real_ger0P x : x \is real ger0_xor_lt0 x `|x| (x < 0) (0 x).

Lemma real_ler0P x : x \is real ler0_xor_gt0 x `|x| (0 < x) (x 0).

Lemma real_ltrgt0P x :
     x \is real
  comparer0 x `|x| (0 == x) (x == 0) (x 0) (0 x) (x < 0) (x > 0).

Lemma real_neqr_lt : {in real &, x y, (x != y) = (x < y) || (y < x)}.

Lemma ler_sub_real x y : x y y - x \is real.

Lemma ger_sub_real x y : x y x - y \is real.

Lemma ler_real y x : x y (x \is real) = (y \is real).

Lemma ger_real x y : y x (x \is real) = (y \is real).

Lemma ger1_real x : 1 x x \is real.
Lemma ler1_real x : x 1 x \is real.

Lemma Nreal_leF x y : y \is real x \notin real (x y) = false.

Lemma Nreal_geF x y : y \is real x \notin real (y x) = false.

Lemma Nreal_ltF x y : y \is real x \notin real (x < y) = false.

Lemma Nreal_gtF x y : y \is real x \notin real (y < x) = false.

real wlog

Lemma real_wlog_ler P :
    ( a b, P b a P a b) ( a b, a b P a b)
   a b : R, a \is real b \is real P a b.

Lemma real_wlog_ltr P :
    ( a, P a a) ( a b, (P b a P a b))
    ( a b, a < b P a b)
   a b : R, a \is real b \is real P a b.

Monotony of addition
Lemma ler_add2l x : {mono +%R x : y z / y z}.

Lemma ler_add2r x : {mono +%R^~ x : y z / y z}.

Lemma ltr_add2r z x y : (x + z < y + z) = (x < y).

Lemma ltr_add2l z x y : (z + x < z + y) = (x < y).

Definition ler_add2 := (ler_add2l, ler_add2r).
Definition ltr_add2 := (ltr_add2l, ltr_add2r).
Definition lter_add2 := (ler_add2, ltr_add2).

Addition, subtraction and transitivity
Lemma ler_add x y z t : x y z t x + z y + t.

Lemma ler_lt_add x y z t : x y z < t x + z < y + t.

Lemma ltr_le_add x y z t : x < y z t x + z < y + t.

Lemma ltr_add x y z t : x < y z < t x + z < y + t.

Lemma ler_sub x y z t : x y t z x - z y - t.

Lemma ler_lt_sub x y z t : x y t < z x - z < y - t.

Lemma ltr_le_sub x y z t : x < y t z x - z < y - t.

Lemma ltr_sub x y z t : x < y t < z x - z < y - t.

Lemma ler_subl_addr x y z : (x - y z) = (x z + y).

Lemma ltr_subl_addr x y z : (x - y < z) = (x < z + y).

Lemma ler_subr_addr x y z : (x y - z) = (x + z y).

Lemma ltr_subr_addr x y z : (x < y - z) = (x + z < y).

Definition ler_sub_addr := (ler_subl_addr, ler_subr_addr).
Definition ltr_sub_addr := (ltr_subl_addr, ltr_subr_addr).
Definition lter_sub_addr := (ler_sub_addr, ltr_sub_addr).

Lemma ler_subl_addl x y z : (x - y z) = (x y + z).

Lemma ltr_subl_addl x y z : (x - y < z) = (x < y + z).

Lemma ler_subr_addl x y z : (x y - z) = (z + x y).

Lemma ltr_subr_addl x y z : (x < y - z) = (z + x < y).

Definition ler_sub_addl := (ler_subl_addl, ler_subr_addl).
Definition ltr_sub_addl := (ltr_subl_addl, ltr_subr_addl).
Definition lter_sub_addl := (ler_sub_addl, ltr_sub_addl).

Lemma ler_addl x y : (x x + y) = (0 y).

Lemma ltr_addl x y : (x < x + y) = (0 < y).

Lemma ler_addr x y : (x y + x) = (0 y).

Lemma ltr_addr x y : (x < y + x) = (0 < y).

Lemma ger_addl x y : (x + y x) = (y 0).

Lemma gtr_addl x y : (x + y < x) = (y < 0).

Lemma ger_addr x y : (y + x x) = (y 0).

Lemma gtr_addr x y : (y + x < x) = (y < 0).

Definition cpr_add := (ler_addl, ler_addr, ger_addl, ger_addl,
                       ltr_addl, ltr_addr, gtr_addl, gtr_addl).

Addition with left member knwon to be positive/negative
Lemma ler_paddl y x z : 0 x y z y x + z.

Lemma ltr_paddl y x z : 0 x y < z y < x + z.

Lemma ltr_spaddl y x z : 0 < x y z y < x + z.

Lemma ltr_spsaddl y x z : 0 < x y < z y < x + z.

Lemma ler_naddl y x z : x 0 y z x + y z.

Lemma ltr_naddl y x z : x 0 y < z x + y < z.

Lemma ltr_snaddl y x z : x < 0 y z x + y < z.

Lemma ltr_snsaddl y x z : x < 0 y < z x + y < z.

Addition with right member we know positive/negative
Lemma ler_paddr y x z : 0 x y z y z + x.

Lemma ltr_paddr y x z : 0 x y < z y < z + x.

Lemma ltr_spaddr y x z : 0 < x y z y < z + x.

Lemma ltr_spsaddr y x z : 0 < x y < z y < z + x.

Lemma ler_naddr y x z : x 0 y z y + x z.

Lemma ltr_naddr y x z : x 0 y < z y + x < z.

Lemma ltr_snaddr y x z : x < 0 y z y + x < z.

Lemma ltr_snsaddr y x z : x < 0 y < z y + x < z.

x and y have the same sign and their sum is null
Lemma paddr_eq0 (x y : R) :
  0 x 0 y (x + y == 0) = (x == 0) && (y == 0).

Lemma naddr_eq0 (x y : R) :
  x 0 y 0 (x + y == 0) = (x == 0) && (y == 0).

Lemma addr_ss_eq0 (x y : R) :
    (0 x) && (0 y) || (x 0) && (y 0)
  (x + y == 0) = (x == 0) && (y == 0).

big sum and ler
Lemma sumr_ge0 I (r : seq I) (P : pred I) (F : I R) :
  ( i, P i (0 F i)) 0 \sum_(i <- r | P i) (F i).

Lemma ler_sum I (r : seq I) (P : pred I) (F G : I R) :
    ( i, P i F i G i)
  \sum_(i <- r | P i) F i \sum_(i <- r | P i) G i.

Lemma psumr_eq0 (I : eqType) (r : seq I) (P : pred I) (F : I R) :
    ( i, P i 0 F i)
  (\sum_(i <- r | P i) (F i) == 0) = (all (fun i(P i) ==> (F i == 0)) r).

:TODO: Cyril : See which form to keep
Lemma psumr_eq0P (I : finType) (P : pred I) (F : I R) :
     ( i, P i 0 F i) \sum_(i | P i) F i = 0
  ( i, P i F i = 0).

mulr and ler/ltr

Lemma ler_pmul2l x : 0 < x {mono *%R x : x y / x y}.

Lemma ltr_pmul2l x : 0 < x {mono *%R x : x y / x < y}.

Definition lter_pmul2l := (ler_pmul2l, ltr_pmul2l).

Lemma ler_pmul2r x : 0 < x {mono *%R^~ x : x y / x y}.

Lemma ltr_pmul2r x : 0 < x {mono *%R^~ x : x y / x < y}.

Definition lter_pmul2r := (ler_pmul2r, ltr_pmul2r).

Lemma ler_nmul2l x : x < 0 {mono *%R x : x y /~ x y}.

Lemma ltr_nmul2l x : x < 0 {mono *%R x : x y /~ x < y}.

Definition lter_nmul2l := (ler_nmul2l, ltr_nmul2l).

Lemma ler_nmul2r x : x < 0 {mono *%R^~ x : x y /~ x y}.

Lemma ltr_nmul2r x : x < 0 {mono *%R^~ x : x y /~ x < y}.

Definition lter_nmul2r := (ler_nmul2r, ltr_nmul2r).

Lemma ler_wpmul2l x : 0 x {homo *%R x : y z / y z}.

Lemma ler_wpmul2r x : 0 x {homo *%R^~ x : y z / y z}.

Lemma ler_wnmul2l x : x 0 {homo *%R x : y z /~ y z}.

Lemma ler_wnmul2r x : x 0 {homo *%R^~ x : y z /~ y z}.

Binary forms, for backchaining.

Lemma ler_pmul x1 y1 x2 y2 :
  0 x1 0 x2 x1 y1 x2 y2 x1 × x2 y1 × y2.

Lemma ltr_pmul x1 y1 x2 y2 :
  0 x1 0 x2 x1 < y1 x2 < y2 x1 × x2 < y1 × y2.

complement for x *+ n and <= or <

Lemma ler_pmuln2r n : (0 < n)%N {mono (@GRing.natmul R)^~ n : x y / x y}.

Lemma ltr_pmuln2r n : (0 < n)%N {mono (@GRing.natmul R)^~ n : x y / x < y}.

Lemma pmulrnI n : (0 < n)%N injective ((@GRing.natmul R)^~ n).

Lemma eqr_pmuln2r n : (0 < n)%N {mono (@GRing.natmul R)^~ n : x y / x == y}.

Lemma pmulrn_lgt0 x n : (0 < n)%N (0 < x *+ n) = (0 < x).

Lemma pmulrn_llt0 x n : (0 < n)%N (x *+ n < 0) = (x < 0).

Lemma pmulrn_lge0 x n : (0 < n)%N (0 x *+ n) = (0 x).

Lemma pmulrn_lle0 x n : (0 < n)%N (x *+ n 0) = (x 0).

Lemma ltr_wmuln2r x y n : x < y (x *+ n < y *+ n) = (0 < n)%N.

Lemma ltr_wpmuln2r n : (0 < n)%N {homo (@GRing.natmul R)^~ n : x y / x < y}.

Lemma ler_wmuln2r n : {homo (@GRing.natmul R)^~ n : x y / x y}.

Lemma mulrn_wge0 x n : 0 x 0 x *+ n.

Lemma mulrn_wle0 x n : x 0 x *+ n 0.

Lemma ler_muln2r n x y : (x *+ n y *+ n) = ((n == 0%N) || (x y)).

Lemma ltr_muln2r n x y : (x *+ n < y *+ n) = ((0 < n)%N && (x < y)).

Lemma eqr_muln2r n x y : (x *+ n == y *+ n) = (n == 0)%N || (x == y).

More characteristic zero properties.

Lemma mulrn_eq0 x n : (x *+ n == 0) = ((n == 0)%N || (x == 0)).

Lemma mulrIn x : x != 0 injective (GRing.natmul x).

Lemma ler_wpmuln2l x :
  0 x {homo (@GRing.natmul R x) : m n / (m n)%N >-> m n}.

Lemma ler_wnmuln2l x :
  x 0 {homo (@GRing.natmul R x) : m n / (n m)%N >-> m n}.

Lemma mulrn_wgt0 x n : 0 < x 0 < x *+ n = (0 < n)%N.

Lemma mulrn_wlt0 x n : x < 0 x *+ n < 0 = (0 < n)%N.

Lemma ler_pmuln2l x :
  0 < x {mono (@GRing.natmul R x) : m n / (m n)%N >-> m n}.

Lemma ltr_pmuln2l x :
  0 < x {mono (@GRing.natmul R x) : m n / (m < n)%N >-> m < n}.

Lemma ler_nmuln2l x :
  x < 0 {mono (@GRing.natmul R x) : m n / (n m)%N >-> m n}.

Lemma ltr_nmuln2l x :
  x < 0 {mono (@GRing.natmul R x) : m n / (n < m)%N >-> m < n}.

Lemma ler_nat m n : (m%:R n%:R :> R) = (m n)%N.

Lemma ltr_nat m n : (m%:R < n%:R :> R) = (m < n)%N.

Lemma eqr_nat m n : (m%:R == n%:R :> R) = (m == n)%N.

Lemma pnatr_eq1 n : (n%:R == 1 :> R) = (n == 1)%N.

Lemma lern0 n : (n%:R 0 :> R) = (n == 0%N).

Lemma ltrn0 n : (n%:R < 0 :> R) = false.

Lemma ler1n n : 1 n%:R :> R = (1 n)%N.
Lemma ltr1n n : 1 < n%:R :> R = (1 < n)%N.
Lemma lern1 n : n%:R 1 :> R = (n 1)%N.
Lemma ltrn1 n : n%:R < 1 :> R = (n < 1)%N.

Lemma ltrN10 : -1 < 0 :> R.
Lemma lerN10 : -1 0 :> R.
Lemma ltr10 : 1 < 0 :> R = false.
Lemma ler10 : 1 0 :> R = false.
Lemma ltr0N1 : 0 < -1 :> R = false.
Lemma ler0N1 : 0 -1 :> R = false.

Lemma pmulrn_rgt0 x n : 0 < x 0 < x *+ n = (0 < n)%N.

Lemma pmulrn_rlt0 x n : 0 < x x *+ n < 0 = false.

Lemma pmulrn_rge0 x n : 0 < x 0 x *+ n.

Lemma pmulrn_rle0 x n : 0 < x x *+ n 0 = (n == 0)%N.

Lemma nmulrn_rgt0 x n : x < 0 0 < x *+ n = false.

Lemma nmulrn_rge0 x n : x < 0 0 x *+ n = (n == 0)%N.

Lemma nmulrn_rle0 x n : x < 0 x *+ n 0.

(x * y) compared to 0 Remark : pmulr_rgt0 and pmulr_rge0 are defined above
x positive and y right
Lemma pmulr_rlt0 x y : 0 < x (x × y < 0) = (y < 0).

Lemma pmulr_rle0 x y : 0 < x (x × y 0) = (y 0).

x positive and y left
Lemma pmulr_lgt0 x y : 0 < x (0 < y × x) = (0 < y).

Lemma pmulr_lge0 x y : 0 < x (0 y × x) = (0 y).

Lemma pmulr_llt0 x y : 0 < x (y × x < 0) = (y < 0).

Lemma pmulr_lle0 x y : 0 < x (y × x 0) = (y 0).

x negative and y right
Lemma nmulr_rgt0 x y : x < 0 (0 < x × y) = (y < 0).

Lemma nmulr_rge0 x y : x < 0 (0 x × y) = (y 0).

Lemma nmulr_rlt0 x y : x < 0 (x × y < 0) = (0 < y).

Lemma nmulr_rle0 x y : x < 0 (x × y 0) = (0 y).

x negative and y left
Lemma nmulr_lgt0 x y : x < 0 (0 < y × x) = (y < 0).

Lemma nmulr_lge0 x y : x < 0 (0 y × x) = (y 0).

Lemma nmulr_llt0 x y : x < 0 (y × x < 0) = (0 < y).

Lemma nmulr_lle0 x y : x < 0 (y × x 0) = (0 y).

weak and symmetric lemmas
Lemma mulr_ge0 x y : 0 x 0 y 0 x × y.

Lemma mulr_le0 x y : x 0 y 0 0 x × y.

Lemma mulr_ge0_le0 x y : 0 x y 0 x × y 0.

Lemma mulr_le0_ge0 x y : x 0 0 y x × y 0.

mulr_gt0 with only one case

Lemma mulr_gt0 x y : 0 < x 0 < y 0 < x × y.

Iterated products

Lemma prodr_ge0 I r (P : pred I) (E : I R) :
  ( i, P i 0 E i) 0 \prod_(i <- r | P i) E i.

Lemma prodr_gt0 I r (P : pred I) (E : I R) :
  ( i, P i 0 < E i) 0 < \prod_(i <- r | P i) E i.

Lemma ler_prod I r (P : pred I) (E1 E2 : I R) :
    ( i, P i 0 E1 i E2 i)
  \prod_(i <- r | P i) E1 i \prod_(i <- r | P i) E2 i.

Lemma ltr_prod I r (P : pred I) (E1 E2 : I R) :
    has P r ( i, P i 0 E1 i < E2 i)
  \prod_(i <- r | P i) E1 i < \prod_(i <- r | P i) E2 i.

Lemma ltr_prod_nat (E1 E2 : nat R) (n m : nat) :
   (m < n)%N ( i, (m i < n)%N 0 E1 i < E2 i)
  \prod_(m i < n) E1 i < \prod_(m i < n) E2 i.

real of mul

Lemma realMr x y : x != 0 x \is real (x × y \is real) = (y \is real).

Lemma realrM x y : y != 0 y \is real (x × y \is real) = (x \is real).

Lemma realM : {in real &, x y, x × y \is real}.

Lemma realrMn x n : (n != 0)%N (x *+ n \is real) = (x \is real).

ler/ltr and multiplication between a positive/negative

Lemma ger_pmull x y : 0 < y (x × y y) = (x 1).

Lemma gtr_pmull x y : 0 < y (x × y < y) = (x < 1).

Lemma ger_pmulr x y : 0 < y (y × x y) = (x 1).

Lemma gtr_pmulr x y : 0 < y (y × x < y) = (x < 1).

Lemma ler_pmull x y : 0 < y (y x × y) = (1 x).

Lemma ltr_pmull x y : 0 < y (y < x × y) = (1 < x).

Lemma ler_pmulr x y : 0 < y (y y × x) = (1 x).

Lemma ltr_pmulr x y : 0 < y (y < y × x) = (1 < x).

Lemma ger_nmull x y : y < 0 (x × y y) = (1 x).

Lemma gtr_nmull x y : y < 0 (x × y < y