Library mathcomp.algebra.ssrnum

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import div fintype path bigop finset fingroup.
From mathcomp Require Import ssralg poly.

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)

rcfType == interface for a real closed field. RcfType T r == packs the real closed axiom r into a rcfType. The carrier T must have a real field type structure. [rcfType of T] == clone of a canonical realClosedFieldType structure on T. [rcfType of T for S ] == T-clone of the realClosedFieldType structure S.

NumClosedField (Partially ordered Closed Field with conjugation)

numClosedFieldType == interface for a closed field with conj. NumClosedFieldType T r == packs the real closed axiom r into a numClosedFieldType. The carrier T must have a closed field type structure. [numClosedFieldType of T] == clone of a canonical numClosedFieldType structure on T [numClosedFieldType of T for S ] == T-clone of the realClosedFieldType structure S.
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. For numeric algebraically closed fields we provide the generic definitions 'i == the imaginary number (:= sqrtC (-1)). 'Re z == the real component of z. 'Im z == the imaginary component of z. z^* == the complex conjugate of z (:= conjC z). sqrtC z == a nonnegative square root of z, i.e., 0 <= sqrt x if 0 <= x. n.-root z == more generally, for n > 0, an nth root of z, chosen with a minimal non-negative argument for n > 1 (i.e., with a maximal real part subject to a nonnegative imaginary part). Note that n.-root (-1) is a primitive 2nth root of unity, an thus not equal to -1 for n odd > 1 (this will be shown in file cyclotomic.v).
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
[arg minr(i < i0 | P) M] == a value i : T minimizing M : R, subject to the condition P (i may appear in P and M), and provided P holds for i0. [arg maxr(i > i0 | P) M] == a value i maximizing M subject to P and provided P holds for i0. [arg minr(i < i0 in A) M] == an i \in A minimizing M if i0 \in A. [arg maxr(i > i0 in A) M] == an i \in A maximizing M if i0 \in A. [arg minr(i < i0) M] == an i : T minimizing M, given i0 : T. [arg maxr(i > i0) M] == an i : T maximizing M, given i0 : T.

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}.
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.
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 m ⇒ Pack (@Class T b m).

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

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}.
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).

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

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.
Canonical join_numDomainType.
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 imaginary_mixin_of (R : numDomainType) := ImaginaryMixin {
  imaginary : R;
  conj_op : {rmorphism R → R};
  _ : imaginary ^+ 2 = - 1;
  _ : ∀ x, x × conj_op x = `|x| ^+ 2;
}.

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

Structure type := Pack {sort; _ : class_of sort}.
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) ⇒
  fun mc ⇒ Pack (@Class T b m mc).
Definition clone := fun b & phant_id class (b : class_of T) ⇒ Pack b.

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

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 numFieldType : type >-> NumField.type.
Canonical numFieldType.
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 T m := (@pack T _ _ id _ _ id m).
Notation "[ 'numClosedFieldType' 'of' T 'for' cT ]" := (@clone T cT _ id)
  (at level 0, format "[ 'numClosedFieldType' 'of' T 'for' cT ]") :
                                                         form_scope.
Notation "[ 'numClosedFieldType' 'of' T ]" := (@clone T _ _ 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}.
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.
Definition pack b0 (m0 : real_axiom (num_for T b0)) :=
  fun bT b & phant_id (NumDomain.class bT) b ⇒
  fun m & phant_id m0 m ⇒ Pack (@Class T b m).

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

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}.
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).

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

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_fieldType.
Canonical join_numFieldType.
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}.
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.
Definition pack b0 (m0 : archimedean_axiom (num_for T b0)) :=
  fun bT b & phant_id (RealField.class bT) b ⇒
  fun m & phant_id m0 m ⇒ Pack (@Class T b m).

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

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}.
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.
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 m ⇒ Pack (@Class T b m).

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

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 then y ^+ 2 == x else y == 0) : bool.

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 : core.

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 : core.
Lemma ltr0Sn n : 0 < n.+1%:R :> R.
Lemma ltr0n n : (0 < n%:R :> R) = (0 < n)%N.
Hint Resolve ltr0Sn : core.

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 : core.

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.

Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0 : core.

Section NumIntegralDomainMonotonyTheory.

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

This listing of "Let"s factor out the required premices for the subsequent lemmas, putting them in the context so that "done" solves the goals quickly

Let leqnn := leqnn.
Let ltnE := ltn_neqAle.
Let ltrE := @ltr_neqAle R.
Let ltr'E := @ltr_neqAle R'.
Let gtnE (m n : nat) : (m > n)%N = (m != n) && (m ≥ n)%N.
Let gtrE (x y : R) : (x > y) = (x != y) && (x ≥ y).
Let gtr'E (x y : R') : (x > y) = (x != y) && (x ≥ y).
Let leq_anti : antisymmetric leq.
Let geq_anti : antisymmetric geq.
Let ler_antiR := @ler_anti R.
Let ler_antiR' := @ler_anti R'.
Let ger_antiR : antisymmetric (>=%R : rel R).
Let ger_antiR' : antisymmetric (>=%R : rel R').
Let leq_total := leq_total.
Let geq_total : total geq.

Section AcrossTypes.

Variables (D D' : {pred R}) (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 inj_homo_ltr :
  injective f → {homo f : x y / x ≤ y} → {homo f : x y / x < y}.

Lemma inj_nhomo_ltr :
  injective f → {homo f : x y /~ x ≤ y} → {homo f : x y /~ x < y}.

Lemma incr_inj : {mono f : x y / x ≤ y} → injective f.

Lemma decr_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 inj_homo_ltr_in :
    {in D & D', injective f} → {in D & D', {homo f : x y / x ≤ y}} →
  {in D & D', {homo f : x y / x < y}}.

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

Lemma incr_inj_in : {in D &, {mono f : x y / x ≤ y}} →
   {in D &, injective f}.

Lemma decr_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.

Variables (D D' : {pred nat}) (f : nat → R).

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

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

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

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

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

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

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

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

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

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

Lemma ltnrW_homo_in : {in D & D', {homo f : m n / (m < n)%N >-> m < n}} →
  {in D & D', {homo f : m n / (m ≤ n)%N >-> m ≤ n}}.

Lemma ltnrW_nhomo_in : {in D & D', {homo f : m n / (n < m)%N >-> m < n}} →
  {in D & D', {homo f : m n / (n ≤ m)%N >-> m ≤ n}}.

Lemma inj_homo_ltnr_in : {in D & D', injective f} →
  {in D & D', {homo f : m n / (m ≤ n)%N >-> m ≤ n}} →
  {in D & D', {homo f : m n / (m < n)%N >-> m < n}}.

Lemma inj_nhomo_ltnr_in : {in D & D', injective f} →
  {in D & D', {homo f : m n / (n ≤ m)%N >-> m ≤ n}} →
  {in D & D', {homo f : m n / (n < m)%N >-> m < n}}.

Lemma incnr_inj_in : {in D &, {mono f : m n / (m ≤ n)%N >-> m ≤ n}} →
  {in D &, injective f}.

Lemma decnr_inj_inj_in : {in D &, {mono f : m n / (n ≤ m)%N >-> m ≤ n}} →
  {in D &, injective f}.

Lemma lenrW_mono_in : {in D &, {mono f : m n / (m ≤ n)%N >-> m ≤ n}} →
  {in D &, {mono f : m n / (m < n)%N >-> m < n}}.

Lemma lenrW_nmono_in : {in D &, {mono f : m n / (n ≤ m)%N >-> m ≤ n}} →
  {in D &, {mono f : m n / (n < m)%N >-> m < n}}.

Lemma lenr_mono_in : {in D &, {homo f : m n / (m < n)%N >-> m < n}} →
   {in D &, {mono f : m n / (m ≤ n)%N >-> m ≤ n}}.

Lemma lenr_nmono_in : {in D &, {homo f : m n / (n < m)%N >-> m < n}} →
  {in D &, {mono f : m n / (n ≤ m)%N >-> m ≤ n}}.

End NatToR.

Section RToNat.

Variables (D D' : {pred R}) (f : R → nat).

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

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

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

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

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

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

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

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

Lemma ltrnW_homo_in : {in D & D', {homo f : m n / m < n >-> (m < n)%N}} →
  {in D & D', {homo f : m n / m ≤ n >-> (m ≤ n)%N}}.

Lemma ltrnW_nhomo_in : {in D & D', {homo f : m n / n < m >-> (m < n)%N}} →
  {in D & D', {homo f : m n / n ≤ m >-> (m ≤ n)%N}}.

Lemma inj_homo_ltrn_in : {in D & D', injective f} →
  {in D & D', {homo f : m n / m ≤ n >-> (m ≤ n)%N}} →
  {in D & D', {homo f : m n / m < n >-> (m < n)%N}}.

Lemma inj_nhomo_ltrn_in : {in D & D', injective f} →
  {in D & D', {homo f : m n / n ≤ m >-> (m ≤ n)%N}} →
  {in D & D', {homo f : m n / n < m >-> (m < n)%N}}.

Lemma incrn_inj_in : {in D &, {mono f : m n / m ≤ n >-> (m ≤ n)%N}} →
  {in D &, injective f}.

Lemma decrn_inj_in : {in D &, {mono f : m n / n ≤ m >-> (m ≤ n)%N}} →
  {in D &, injective f}.

Lemma lernW_mono_in : {in D &, {mono f : m n / m ≤ n >-> (m ≤ n)%N}} →
  {in D &, {mono f : m n / m < n >-> (m < n)%N}}.

Lemma lernW_nmono_in : {in D &, {mono f : m n / n ≤ m >-> (m ≤ n)%N}} →
  {in D &, {mono f : m n / n < m >-> (m < n)%N}}.

End RToNat.

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 : core.
Lemma ltr_opp2 : {mono -%R : x y /~ x < y :> R}.
Hint Resolve ltr_opp2 : core.
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 : core.

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

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

Variant 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.

Variant 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.

Variant 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).

Variant 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.

Variant 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.

Variant 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_add2l x : {mono +%R x : y z / y < z}.

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

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) = (1 < x).

Lemma ger_nmulr x y : y < 0 → (y × x ≤ y) = (1 ≤ x).

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

Lemma ler_nmull x y : y < 0 → (y ≤ x × y) = (x ≤ 1).

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

Lemma ler_nmulr x y : y < 0 → (y ≤ y × x) = (x ≤ 1).

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

ler/ltr and multiplication between a positive/negative and a exterior (1 <= _) or interior (0 <= _ <= 1)

Lemma ler_pemull x y : 0 ≤ y → 1 ≤ x → y ≤ x × y.

Lemma ler_nemull x y : y ≤ 0 → 1 ≤ x → x × y ≤ y.

Lemma ler_pemulr x y : 0 ≤ y → 1 ≤ x → y ≤ y × x.

Lemma ler_nemulr x y : y ≤ 0 → 1 ≤ x → y × x ≤ y.

Lemma ler_pimull x y : 0 ≤ y → x ≤ 1 → x × y ≤ y.

Lemma ler_nimull x y : y ≤ 0 → x ≤ 1 → y ≤ x × y.

Lemma ler_pimulr x y : 0 ≤ y → x ≤ 1 → y × x ≤ y.

Lemma ler_nimulr x y : y ≤ 0 → x ≤ 1 → y ≤ y × x.

Lemma mulr_ile1 x y : 0 ≤ x → 0 ≤ y → x ≤ 1 → y ≤ 1 → x × y ≤ 1.

Lemma mulr_ilt1 x y : 0 ≤ x → 0 ≤ y → x < 1 → y < 1 → x × y < 1.

Definition mulr_ilte1 := (mulr_ile1, mulr_ilt1).

Lemma mulr_ege1 x y : 1 ≤ x → 1 ≤ y → 1 ≤ x × y.

Lemma mulr_egt1 x y : 1 < x → 1 < y → 1 < x × y.
Definition mulr_egte1 := (mulr_ege1, mulr_egt1).
Definition mulr_cp1 := (mulr_ilte1, mulr_egte1).

ler and ^-1

Lemma invr_gt0 x : (0 < x^-1) = (0 < x).

Lemma invr_ge0 x : (0 ≤ x^-1) = (0 ≤ x).

Lemma invr_lt0 x : (x^-1 < 0) = (x < 0).

Lemma invr_le0 x : (x^-1 ≤ 0) = (x ≤ 0).

Definition invr_gte0 := (invr_ge0, invr_gt0).
Definition invr_lte0 := (invr_le0, invr_lt0).

Lemma divr_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x / y.

Lemma divr_gt0 x y : 0 < x → 0 < y → 0 < x / y.

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

ler and exprn
Lemma exprn_ge0 n x : 0 ≤ x → 0 ≤ x ^+ n.

Lemma realX n : {in real, ∀ x, x ^+ n \is real}.

Lemma exprn_gt0 n x : 0 < x → 0 < x ^+ n.

Definition exprn_gte0 := (exprn_ge0, exprn_gt0).

Lemma exprn_ile1 n x : 0 ≤ x → x ≤ 1 → x ^+ n ≤ 1.

Lemma exprn_ilt1 n x : 0 ≤ x → x < 1 → x ^+ n < 1 = (n != 0%N).

Definition exprn_ilte1 := (exprn_ile1, exprn_ilt1).

Lemma exprn_ege1 n x : 1 ≤ x → 1 ≤ x ^+ n.

Lemma exprn_egt1 n x : 1 < x → 1 < x ^+ n = (n != 0%N).

Definition exprn_egte1 := (exprn_ege1, exprn_egt1).
Definition exprn_cp1 := (exprn_ilte1, exprn_egte1).

Lemma ler_iexpr x n : (0 < n)%N → 0 ≤ x → x ≤ 1 → x ^+ n ≤ x.

Lemma ltr_iexpr x n : 0 < x → x < 1 → (x ^+ n < x) = (1 < n)%N.

Definition lter_iexpr := (ler_iexpr, ltr_iexpr).

Lemma ler_eexpr x n : (0 < n)%N → 1 ≤ x → x ≤ x ^+ n.

Lemma ltr_eexpr x n : 1 < x → (x < x ^+ n) = (1 < n)%N.

Definition lter_eexpr := (ler_eexpr, ltr_eexpr).
Definition lter_expr := (lter_iexpr, lter_eexpr).

Lemma ler_wiexpn2l x :
  0 ≤ x → x ≤ 1 → {homo (GRing.exp x) : m n / (n ≤ m)%N >-> m ≤ n}.

Lemma ler_weexpn2l x :
  1 ≤ x → {homo (GRing.exp x) : m n / (m ≤ n)%N >-> m ≤ n}.

Lemma ieexprn_weq1 x n : 0 ≤ x → (x ^+ n == 1) = ((n == 0%N) || (x == 1)).

Lemma ieexprIn x : 0 < x → x != 1 → injective (GRing.exp x).

Lemma ler_iexpn2l x :
  0 < x → x < 1 → {mono (GRing.exp x) : m n / (n ≤ m)%N >-> m ≤ n}.

Lemma ltr_iexpn2l x :
  0 < x → x < 1 → {mono (GRing.exp x) : m n / (n < m)%N >-> m < n}.

Definition lter_iexpn2l := (ler_iexpn2l, ltr_iexpn2l).

Lemma ler_eexpn2l x :
  1 < x → {mono (GRing.exp x) : m n / (m ≤ n)%N >-> m ≤ n}.

Lemma ltr_eexpn2l x :
  1 < x → {mono (GRing.exp x) : m n / (m < n)%N >-> m < n}.

Definition lter_eexpn2l := (ler_eexpn2l, ltr_eexpn2l).

Lemma ltr_expn2r n x y : 0 ≤ x → x < y → x ^+ n < y ^+ n = (n != 0%N).

Lemma ler_expn2r n : {in nneg & , {homo ((@GRing.exp R)^~ n) : x y / x ≤ y}}.

Definition lter_expn2r := (ler_expn2r, ltr_expn2r).

Lemma ltr_wpexpn2r n :
  (0 < n)%N → {in nneg & , {homo ((@GRing.exp R)^~ n) : x y / x < y}}.

Lemma ler_pexpn2r n :
  (0 < n)%N → {in nneg & , {mono ((@GRing.exp R)^~ n) : x y / x ≤ y}}.

Lemma ltr_pexpn2r n :
  (0 < n)%N → {in nneg & , {mono ((@GRing.exp R)^~ n) : x y / x < y}}.

Definition lter_pexpn2r := (ler_pexpn2r, ltr_pexpn2r).

Lemma pexpIrn n : (0 < n)%N → {in nneg &, injective ((@GRing.exp R)^~ n)}.

expr and ler/ltr
Lemma expr_le1 n x : (0 < n)%N → 0 ≤ x → (x ^+ n ≤ 1) = (x ≤ 1).

Lemma expr_lt1 n x : (0 < n)%N → 0 ≤ x → (x ^+ n < 1) = (x < 1).

Definition expr_lte1 := (expr_le1, expr_lt1).

Lemma expr_ge1 n x : (0 < n)%N → 0 ≤ x → (1 ≤ x ^+ n) = (1 ≤ x).

Lemma expr_gt1 n x : (0 < n)%N → 0 ≤ x → (1 < x ^+ n) = (1 < x).

Definition expr_gte1 := (expr_ge1, expr_gt1).

Lemma pexpr_eq1 x n : (0 < n)%N → 0 ≤ x → (x ^+ n == 1) = (x == 1).

Lemma pexprn_eq1 x n : 0 ≤ x → (x ^+ n == 1) = (n == 0%N) || (x == 1).

Lemma eqr_expn2 n x y :
  (0 < n)%N → 0 ≤ x → 0 ≤ y → (x ^+ n == y ^+ n) = (x == y).

Lemma sqrp_eq1 x : 0 ≤ x → (x ^+ 2 == 1) = (x == 1).

Lemma sqrn_eq1 x : x ≤ 0 → (x ^+ 2 == 1) = (x == -1).

Lemma ler_sqr : {in nneg &, {mono (fun x ⇒ x ^+ 2) : x y / x ≤ y}}.

Lemma ltr_sqr : {in nneg &, {mono (fun x ⇒ x ^+ 2) : x y / x < y}}.

Lemma ler_pinv :
  {in [pred x in GRing.unit | 0 < x] &, {mono (@GRing.inv R) : x y /~ x ≤ y}}.

Lemma ler_ninv :
  {in [pred x in GRing.unit | x < 0] &, {mono (@GRing.inv R) : x y /~ x ≤ y}}.

Lemma ltr_pinv :
  {in [pred x in GRing.unit | 0 < x] &, {mono (@GRing.inv R) : x y /~ x < y}}.

Lemma ltr_ninv :
  {in [pred x in GRing.unit | x < 0] &, {mono (@GRing.inv R) : x y /~ x < y}}.

Lemma invr_gt1 x : x \is a GRing.unit → 0 < x → (1 < x^-1) = (x < 1).

Lemma invr_ge1 x : x \is a GRing.unit → 0 < x → (1 ≤ x^-1) = (x ≤ 1).

Definition invr_gte1 := (invr_ge1, invr_gt1).

Lemma invr_le1 x (ux : x \is a GRing.unit) (hx : 0 < x) :
  (x^-1 ≤ 1) = (1 ≤ x).

Lemma invr_lt1 x (ux : x \is a GRing.unit) (hx : 0 < x) : (x^-1 < 1) = (1 < x).

Definition invr_lte1 := (invr_le1, invr_lt1).
Definition invr_cp1 := (invr_gte1, invr_lte1).

norm

Lemma real_ler_norm x : x \is real → x ≤ `|x|.

norm + add

Lemma normr_real x : `|x| \is real.
Hint Resolve normr_real : core.

Lemma ler_norm_sum I r (G : I → R) (P : pred I):
  `|\sum_(i <- r | P i) G i| ≤ \sum_(i <- r | P i) `|G i|.

Lemma ler_norm_sub x y : `|x - y| ≤ `|x| + `|y|.

Lemma ler_dist_add z x y : `|x - y| ≤ `|x - z| + `|z - y|.

Lemma ler_sub_norm_add x y : `|x| - `|y| ≤ `|x + y|.

Lemma ler_sub_dist x y : `|x| - `|y| ≤ `|x - y|.

Lemma ler_dist_dist x y : `|`|x| - `|y| | ≤ `|x - y|.

Lemma ler_dist_norm_add x y : `| `|x| - `|y| | ≤ `| x + y |.

Lemma real_ler_norml x y : x \is real → (`|x| ≤ y) = (- y ≤ x ≤ y).

Lemma real_ler_normlP x y :
  x \is real → reflect ((-x ≤ y) × (x ≤ y)) (`|x| ≤ y).

Lemma real_eqr_norml x y :
  x \is real → (`|x| == y) = ((x == y) || (x == -y)) && (0 ≤ y).

Lemma real_eqr_norm2 x y :
  x \is real → y \is real → (`|x| == `|y|) = (x == y) || (x == -y).

Lemma real_ltr_norml x y : x \is real → (`|x| < y) = (- y < x < y).

Definition real_lter_norml := (real_ler_norml, real_ltr_norml).

Lemma real_ltr_normlP x y :
  x \is real → reflect ((-x < y) × (x < y)) (`|x| < y).

Lemma real_ler_normr x y : y \is real → (x ≤ `|y|) = (x ≤ y) || (x ≤ - y).

Lemma real_ltr_normr x y : y \is real → (x < `|y|) = (x < y) || (x < - y).

Definition real_lter_normr := (real_ler_normr, real_ltr_normr).

Lemma ler_nnorml x y : y < 0 → `|x| ≤ y = false.

Lemma ltr_nnorml x y : y ≤ 0 → `|x| < y = false.

Definition lter_nnormr := (ler_nnorml, ltr_nnorml).

Lemma real_ler_distl x y e :
  x - y \is real → (`|x - y| ≤ e) = (y - e ≤ x ≤ y + e).

Lemma real_ltr_distl x y e :
  x - y \is real → (`|x - y| < e) = (y - e < x < y + e).

Definition real_lter_distl := (real_ler_distl, real_ltr_distl).

(* GG: pointless duplication }-( *)
Lemma eqr_norm_id x : (`|x| == x) = (0 ≤ x).
Lemma eqr_normN x : (`|x| == - x) = (x ≤ 0).
Definition eqr_norm_idVN := =^~ (ger0_def, ler0_def).

Lemma real_exprn_even_ge0 n x : x \is real → ~~ odd n → 0 ≤ x ^+ n.

Lemma real_exprn_even_gt0 n x :
  x \is real → ~~ odd n → (0 < x ^+ n) = (n == 0)%N || (x != 0).

Lemma real_exprn_even_le0 n x :
  x \is real → ~~ odd n → (x ^+ n ≤ 0) = (n != 0%N) && (x == 0).

Lemma real_exprn_even_lt0 n x :
  x \is real → ~~ odd n → (x ^+ n < 0) = false.

Lemma real_exprn_odd_ge0 n x :
  x \is real → odd n → (0 ≤ x ^+ n) = (0 ≤ x).

Lemma real_exprn_odd_gt0 n x : x \is real → odd n → (0 < x ^+ n) = (0 < x).

Lemma real_exprn_odd_le0 n x : x \is real → odd n → (x ^+ n ≤ 0) = (x ≤ 0).

Lemma real_exprn_odd_lt0 n x : x \is real → odd n → (x ^+ n < 0) = (x < 0).

GG: Could this be a better definition of "real" ?
Lemma realEsqr x : (x \is real) = (0 ≤ x ^+ 2).

Lemma real_normK x : x \is real → `|x| ^+ 2 = x ^+ 2.

Binary sign ((-1) ^+ s).

Lemma normr_sign s : `|(-1) ^+ s| = 1 :> R.

Lemma normrMsign s x : `|(-1) ^+ s × x| = `|x|.

Lemma signr_gt0 (b : bool) : (0 < (-1) ^+ b :> R) = ~~ b.

Lemma signr_lt0 (b : bool) : ((-1) ^+ b < 0 :> R) = b.

Lemma signr_ge0 (b : bool) : (0 ≤ (-1) ^+ b :> R) = ~~ b.

Lemma signr_le0 (b : bool) : ((-1) ^+ b ≤ 0 :> R) = b.

This actually holds for char R != 2.
Lemma signr_inj : injective (fun b : bool ⇒ (-1) ^+ b : R).

Ternary sign (sg).

Lemma sgr_def x : sg x = (-1) ^+ (x < 0)%R *+ (x != 0).

Lemma neqr0_sign x : x != 0 → (-1) ^+ (x < 0)%R = sgr x.

Lemma gtr0_sg x : 0 < x → sg x = 1.

Lemma ltr0_sg x : x < 0 → sg x = -1.

Lemma sgr0 : sg 0 = 0 :> R.
Lemma sgr1 : sg 1 = 1 :> R.
Lemma sgrN1 : sg (-1) = -1 :> R.
Definition sgrE := (sgr0, sgr1, sgrN1).

Lemma sqr_sg x : sg x ^+ 2 = (x != 0)%:R.

Lemma mulr_sg_eq1 x y : (sg x × y == 1) = (x != 0) && (sg x == y).

Lemma mulr_sg_eqN1 x y : (sg x × sg y == -1) = (x != 0) && (sg x == - sg y).

Lemma sgr_eq0 x : (sg x == 0) = (x == 0).

Lemma sgr_odd n x : x != 0 → (sg x) ^+ n = (sg x) ^+ (odd n).

Lemma sgrMn x n : sg (x *+ n) = (n != 0%N)%:R × sg x.

Lemma sgr_nat n : sg n%:R = (n != 0%N)%:R :> R.

Lemma sgr_id x : sg (sg x) = sg x.

Lemma sgr_lt0 x : (sg x < 0) = (x < 0).

Lemma sgr_le0 x : (sgr x ≤ 0) = (x ≤ 0).

sign and norm

Lemma realEsign x : x \is real → x = (-1) ^+ (x < 0)%R × `|x|.

Lemma realNEsign x : x \is real → - x = (-1) ^+ (0 < x)%R × `|x|.

Lemma real_normrEsign (x : R) (xR : x \is real) : `|x| = (-1) ^+ (x < 0)%R × x.

GG: pointless duplication...
Lemma real_mulr_sign_norm x : x \is real → (-1) ^+ (x < 0)%R × `|x| = x.

Lemma real_mulr_Nsign_norm x : x \is real → (-1) ^+ (0 < x)%R × `|x| = - x.

Lemma realEsg x : x \is real → x = sgr x × `|x|.

Lemma normr_sg x : `|sg x| = (x != 0)%:R.

Lemma sgr_norm x : sg `|x| = (x != 0)%:R.

lerif

Lemma lerif_refl x C : reflect (x ≤ x ?= iff C) C.

Lemma lerif_trans x1 x2 x3 C12 C23 :
  x1 ≤ x2 ?= iff C12 → x2 ≤ x3 ?= iff C23 → x1 ≤ x3 ?= iff C12 && C23.

Lemma lerif_le x y : x ≤ y → x ≤ y ?= iff (x ≥ y).

Lemma lerif_eq x y : x ≤ y → x ≤ y ?= iff (x == y).

Lemma ger_lerif x y C : x ≤ y ?= iff C → (y ≤ x) = C.

Lemma ltr_lerif x y C : x ≤ y ?= iff C → (x < y) = ~~ C.

Lemma lerif_nat m n C : (m%:R ≤ n%:R ?= iff C :> R) = (m ≤ n ?= iff C)%N.

Lemma mono_in_lerif (A : {pred R}) (f : R → R) C :
   {in A &, {mono f : x y / x ≤ y}} →
  {in A &, ∀ x y, (f x ≤ f y ?= iff C) = (x ≤ y ?= iff C)}.

Lemma mono_lerif (f : R → R) C :
    {mono f : x y / x ≤ y} →
  ∀ x y, (f x ≤ f y ?= iff C) = (x ≤ y ?= iff C).

Lemma nmono_in_lerif (A : {pred R}) (f : R → R) C :
    {in A &, {mono f : x y /~ x ≤ y}} →
  {in A &, ∀ x y, (f x ≤ f y ?= iff C) = (y ≤ x ?= iff C)}.

Lemma nmono_lerif (f : R → R) C :
    {mono f : x y /~ x ≤ y} →
  ∀ x y, (f x ≤ f y ?= iff C) = (y ≤ x ?= iff C).

Lemma lerif_subLR x y z C : (x - y ≤ z ?= iff C) = (x ≤ z + y ?= iff C).

Lemma lerif_subRL x y z C : (x ≤ y - z ?= iff C) = (x + z ≤ y ?= iff C).

Lemma lerif_add x1 y1 C1 x2 y2 C2 :
    x1 ≤ y1 ?= iff C1 → x2 ≤ y2 ?= iff C2 →
  x1 + x2 ≤ y1 + y2 ?= iff C1 && C2.

Lemma lerif_sum (I : finType) (P C : pred I) (E1 E2 : I → R) :
    (∀ i, P i → E1 i ≤ E2 i ?= iff C i) →
  \sum_(i | P i) E1 i ≤ \sum_(i | P i) E2 i ?= iff [∀ (i | P i), C i].

Lemma lerif_0_sum (I : finType) (P C : pred I) (E : I → R) :
    (∀ i, P i → 0 ≤ E i ?= iff C i) →
  0 ≤ \sum_(i | P i) E i ?= iff [∀ (i | P i), C i].

Lemma real_lerif_norm x : x \is real → x ≤ `|x| ?= iff (0 ≤ x).

Lemma lerif_pmul x1 x2 y1 y2 C1 C2 :
    0 ≤ x1 → 0 ≤ x2 → x1 ≤ y1 ?= iff C1 → x2 ≤ y2 ?= iff C2 →
  x1 × x2 ≤ y1 × y2 ?= iff (y1 × y2 == 0) || C1 && C2.

Lemma lerif_nmul x1 x2 y1 y2 C1 C2 :
    y1 ≤ 0 → y2 ≤ 0 → x1 ≤ y1 ?= iff C1 → x2 ≤ y2 ?= iff C2 →
  y1 × y2 ≤ x1 × x2 ?= iff (x1 × x2 == 0) || C1 && C2.

Lemma lerif_pprod (I : finType) (P C : pred I) (E1 E2 : I → R) :
    (∀ i, P i → 0 ≤ E1 i) →
    (∀ i, P i → E1 i ≤ E2 i ?= iff C i) →
  let pi E := \prod_(i | P i) E i in
  pi E1 ≤ pi E2 ?= iff (pi E2 == 0) || [∀ (i | P i), C i].

Mean inequalities.

Lemma real_lerif_mean_square_scaled x y :
  x \is real → y \is real → x × y *+ 2 ≤ x ^+ 2 + y ^+ 2 ?= iff (x == y).

Lemma real_lerif_AGM2_scaled x y :
  x \is real → y \is real → x × y *+ 4 ≤ (x + y) ^+ 2 ?= iff (x == y).

Lemma lerif_AGM_scaled (I : finType) (A : {pred I}) (E : I → R) (n := #|A|) :
    {in A, ∀ i, 0 ≤ E i *+ n} →
  \prod_(i in A) (E i *+ n) ≤ (\sum_(i in A) E i) ^+ n
                            ?= iff [∀ i in A, ∀ j in A, E i == E j].

Polynomial bound.

Implicit Type p : {poly R}.

Lemma poly_disk_bound p b : {ub | ∀ x, `|x| ≤ b → `|p.[x]| ≤ ub}.

End NumDomainOperationTheory.

Hint Resolve ler_opp2 ltr_opp2 real0 real1 normr_real : core.

Section NumDomainMonotonyTheoryForReals.

Variables (R R' : numDomainType) (D : pred R) (f : R → R') (f' : R → nat).
Implicit Types (m n p : nat) (x y z : R) (u v w : R').

Lemma real_mono :
  {homo f : x y / x < y} → {in real &, {mono f : x y / x ≤ y}}.

Lemma real_nmono :
  {homo f : x y /~ x < y} → {in real &, {mono f : x y /~ x ≤ y}}.

Lemma real_mono_in :
    {in D &, {homo f : x y / x < y}} →
  {in [pred x in D | x \is real] &, {mono f : x y / x ≤ y}}.

Lemma real_nmono_in :
    {in D &, {homo f : x y /~ x < y}} →
  {in [pred x in D | x \is real] &, {mono f : x y /~ x ≤ y}}.

Lemma realn_mono : {homo f' : x y / x < y >-> (x < y)%N} →
  {in real &, {mono f' : x y / x ≤ y >-> (x ≤ y)%N}}.

Lemma realn_nmono : {homo f' : x y / y < x >-> (x < y)%N} →
  {in real &, {mono f' : x y / y ≤ x >-> (x ≤ y)%N}}.

Lemma realn_mono_in : {in D &, {homo f' : x y / x < y >-> (x < y)%N}} →
  {in [pred x in D | x \is real] &, {mono f' : x y / x ≤ y >-> (x ≤ y)%N}}.

Lemma realn_nmono_in : {in D &, {homo f' : x y / y < x >-> (x < y)%N}} →
  {in [pred x in D | x \is real] &, {mono f' : x y / y ≤ x >-> (x ≤ y)%N}}.

End NumDomainMonotonyTheoryForReals.

Section FinGroup.

Import GroupScope.

Variables (R : numDomainType) (gT : finGroupType).
Implicit Types G : {group gT}.

Lemma natrG_gt0 G : #|G|%:R > 0 :> R.

Lemma natrG_neq0 G : #|G|%:R != 0 :> R.

Lemma natr_indexg_gt0 G B : #|G : B|%:R > 0 :> R.

Lemma natr_indexg_neq0 G B : #|G : B|%:R != 0 :> R.

End FinGroup.

Section NumFieldTheory.

Variable F : numFieldType.
Implicit Types x y z t : F.

Lemma unitf_gt0 x : 0 < x → x \is a GRing.unit.

Lemma unitf_lt0 x : x < 0 → x \is a GRing.unit.

Lemma lef_pinv : {in pos &, {mono (@GRing.inv F) : x y /~ x ≤ y}}.

Lemma lef_ninv : {in neg &, {mono (@GRing.inv F) : x y /~ x ≤ y}}.

Lemma ltf_pinv : {in pos &, {mono (@GRing.inv F) : x y /~ x < y}}.

Lemma ltf_ninv: {in neg &, {mono (@GRing.inv F) : x y /~ x < y}}.

Definition ltef_pinv := (lef_pinv, ltf_pinv).
Definition ltef_ninv := (lef_ninv, ltf_ninv).

Lemma invf_gt1 x : 0 < x → (1 < x^-1) = (x < 1).

Lemma invf_ge1 x : 0 < x → (1 ≤ x^-1) = (x ≤ 1).

Definition invf_gte1 := (invf_ge1, invf_gt1).

Lemma invf_le1 x : 0 < x → (x^-1 ≤ 1) = (1 ≤ x).

Lemma invf_lt1 x : 0 < x → (x^-1 < 1) = (1 < x).

Definition invf_lte1 := (invf_le1, invf_lt1).
Definition invf_cp1 := (invf_gte1, invf_lte1).

These lemma are all combinations of mono(LR|RL) with ler [pn]mul2[rl].
Lemma ler_pdivl_mulr z x y : 0 < z → (x ≤ y / z) = (x × z ≤ y).

Lemma ltr_pdivl_mulr z x y : 0 < z → (x < y / z) = (x × z < y).

Definition lter_pdivl_mulr := (ler_pdivl_mulr, ltr_pdivl_mulr).

Lemma ler_pdivr_mulr z x y : 0 < z → (y / z ≤ x) = (y ≤ x × z).

Lemma ltr_pdivr_mulr z x y : 0 < z → (y / z < x) = (y < x × z).

Definition lter_pdivr_mulr := (ler_pdivr_mulr, ltr_pdivr_mulr).

Lemma ler_pdivl_mull z x y : 0 < z → (x ≤ z^-1 × y) = (z × x ≤ y).

Lemma ltr_pdivl_mull z x y : 0 < z → (x < z^-1 × y) = (z × x < y).

Definition lter_pdivl_mull := (ler_pdivl_mull, ltr_pdivl_mull).

Lemma ler_pdivr_mull z x y : 0 < z → (z^-1 × y ≤ x) = (y ≤ z × x).

Lemma ltr_pdivr_mull z x y : 0 < z → (z^-1 × y < x) = (y < z × x).

Definition lter_pdivr_mull := (ler_pdivr_mull, ltr_pdivr_mull).

Lemma ler_ndivl_mulr z x y : z < 0 → (x ≤ y / z) = (y ≤ x × z).

Lemma ltr_ndivl_mulr z x y : z < 0 → (x < y / z) = (y < x × z).

Definition lter_ndivl_mulr := (ler_ndivl_mulr, ltr_ndivl_mulr).

Lemma ler_ndivr_mulr z x y : z < 0 → (y / z ≤ x) = (x × z ≤ y).

Lemma ltr_ndivr_mulr z x y : z < 0 → (y / z < x) = (x × z < y).

Definition lter_ndivr_mulr := (ler_ndivr_mulr, ltr_ndivr_mulr).

Lemma ler_ndivl_mull z x y : z < 0 → (x ≤ z^-1 × y) = (y ≤ z × x).

Lemma ltr_ndivl_mull z x y : z < 0 → (x < z^-1 × y) = (y < z × x).

Definition lter_ndivl_mull := (ler_ndivl_mull, ltr_ndivl_mull).

Lemma ler_ndivr_mull z x y : z < 0 → (z^-1 × y ≤ x) = (z × x ≤ y).

Lemma ltr_ndivr_mull z x y : z < 0 → (z^-1 × y < x) = (z × x < y).

Definition lter_ndivr_mull := (ler_ndivr_mull, ltr_ndivr_mull).

Lemma natf_div m d : (d %| m)%N → (m %/ d)%:R = m%:R / d%:R :> F.

Lemma normfV : {morph (@norm F) : x / x ^-1}.

Lemma normf_div : {morph (@norm F) : x y / x / y}.

Lemma invr_sg x : (sg x)^-1 = sgr x.

Lemma sgrV x : sgr x^-1 = sgr x.

Interval midpoint.


Lemma midf_le x y : x ≤ y → (x ≤ mid x y) × (mid x y ≤ y).

Lemma midf_lt x y : x < y → (x < mid x y) × (mid x y < y).

Definition midf_lte := (midf_le, midf_lt).

The AGM, unscaled but without the nth root.

Lemma real_lerif_mean_square x y :
  x \is real → y \is real → x × y ≤ mid (x ^+ 2) (y ^+ 2) ?= iff (x == y).

Lemma real_lerif_AGM2 x y :
  x \is real → y \is real → x × y ≤ mid x y ^+ 2 ?= iff (x == y).

Lemma lerif_AGM (I : finType) (A : {pred I}) (E : I → F) :
    let n := #|A| in let mu := (\sum_(i in A) E i) / n%:R in
    {in A, ∀ i, 0 ≤ E i} →
  \prod_(i in A) E i ≤ mu ^+ n
                     ?= iff [∀ i in A, ∀ j in A, E i == E j].

Implicit Type p : {poly F}.
Lemma Cauchy_root_bound p : p != 0 → {b | ∀ x, root p x → `|x| ≤ b}.

Import GroupScope.

Lemma natf_indexg (gT : finGroupType) (G H : {group gT}) :
  H \subset G → #|G : H|%:R = (#|G|%:R / #|H|%:R)%R :> F.

End NumFieldTheory.

Section RealDomainTheory.

Hint Resolve lerr : core.

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

Lemma num_real x : x \is real.
Hint Resolve num_real : core.

Lemma ler_total : total (@le R).

Lemma ltr_total x y : x != y → (x < y) || (y < x).

Lemma wlog_ler P :
     (∀ a b, P b a → P a b) → (∀ a b, a ≤ b → P a b) →
   ∀ a b : R, P a b.

Lemma 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, P a b.

Lemma ltrNge x y : (x < y) = ~~ (y ≤ x).

Lemma lerNgt x y : (x ≤ y) = ~~ (y < x).

Lemma lerP x y : ler_xor_gt x y `|x - y| `|y - x| (x ≤ y) (y < x).

Lemma ltrP x y : ltr_xor_ge x y `|x - y| `|y - x| (y ≤ x) (x < y).

Lemma ltrgtP x y :
   comparer x y `|x - y| `|y - x| (y == x) (x == y)
                 (x ≤ y) (y ≤ x) (x < y) (x > y) .

Lemma ger0P x : ger0_xor_lt0 x `|x| (x < 0) (0 ≤ x).

Lemma ler0P x : ler0_xor_gt0 x `|x| (0 < x) (x ≤ 0).

Lemma ltrgt0P x :
  comparer0 x `|x| (0 == x) (x == 0) (x ≤ 0) (0 ≤ x) (x < 0) (x > 0).

Lemma neqr_lt x y : (x != y) = (x < y) || (y < x).

Lemma eqr_leLR x y z t :
  (x ≤ y → z ≤ t) → (y < x → t < z) → (x ≤ y) = (z ≤ t).

Lemma eqr_leRL x y z t :
  (x ≤ y → z ≤ t) → (y < x → t < z) → (z ≤ t) = (x ≤ y).

Lemma eqr_ltLR x y z t :
  (x < y → z < t) → (y ≤ x → t ≤ z) → (x < y) = (z < t).

Lemma eqr_ltRL x y z t :
  (x < y → z < t) → (y ≤ x → t ≤ z) → (z < t) = (x < y).

sign

Lemma mulr_lt0 x y :
  (x × y < 0) = [&& x != 0, y != 0 & (x < 0) (+) (y < 0)].

Lemma neq0_mulr_lt0 x y :
  x != 0 → y != 0 → (x × y < 0) = (x < 0) (+) (y < 0).

Lemma mulr_sign_lt0 (b : bool) x :
  ((-1) ^+ b × x < 0) = (x != 0) && (b (+) (x < 0)%R).

sign & norm

Lemma mulr_sign_norm x : (-1) ^+ (x < 0)%R × `|x| = x.

Lemma mulr_Nsign_norm x : (-1) ^+ (0 < x)%R × `|x| = - x.

Lemma numEsign x : x = (-1) ^+ (x < 0)%R × `|x|.

Lemma numNEsign x : -x = (-1) ^+ (0 < x)%R × `|x|.

Lemma normrEsign x : `|x| = (-1) ^+ (x < 0)%R × x.

End RealDomainTheory.

Hint Resolve num_real : core.

Section RealDomainMonotony.

Variables (R : realDomainType) (R' : numDomainType) (D : pred R).
Variables (f : R → R') (f' : R → nat).
Implicit Types (m n p : nat) (x y z : R) (u v w : R').

Hint Resolve (@num_real R) : core.

Lemma ler_mono : {homo f : x y / x < y} → {mono f : x y / x ≤ y}.

Lemma ler_nmono : {homo f : x y /~ x < y} → {mono f : x y /~ x ≤ y}.

Lemma ler_mono_in :
  {in D &, {homo f : x y / x < y}} → {in D &, {mono f : x y / x ≤ y}}.

Lemma ler_nmono_in :
  {in D &, {homo f : x y /~ x < y}} → {in D &, {mono f : x y /~ x ≤ y}}.

Lemma lern_mono : {homo f' : m n / m < n >-> (m < n)%N} →
   {mono f' : m n / m ≤ n >-> (m ≤ n)%N}.

Lemma lern_nmono : {homo f' : m n / n < m >-> (m < n)%N} →
  {mono f' : m n / n ≤ m >-> (m ≤ n)%N}.

Lemma lern_mono_in : {in D &, {homo f' : m n / m < n >-> (m < n)%N}} →
   {in D &, {mono f' : m n / m ≤ n >-> (m ≤ n)%N}}.

Lemma lern_nmono_in : {in D &, {homo f' : m n / n < m >-> (m < n)%N}} →
  {in D &, {mono f' : m n / n ≤ m >-> (m ≤ n)%N}}.

End RealDomainMonotony.

Section RealDomainArgExtremum.

Context {R : realDomainType} {I : finType} (i0 : I).
Context (P : pred I) (F : I → R) (Pi0 : P i0).

Definition arg_minr := extremum <=%R i0 P F.
Definition arg_maxr := extremum >=%R i0 P F.

Lemma arg_minrP: extremum_spec <=%R P F arg_minr.

Lemma arg_maxrP: extremum_spec >=%R P F arg_maxr.

End RealDomainArgExtremum.

Notation "[ 'arg' 'minr_' ( i < i0 | P ) F ]" :=
    (arg_minr i0 (fun i ⇒ P%B) (fun i ⇒ F))
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'minr_' ( i < i0 | P ) F ]") : form_scope.

Notation "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]" :=
    [arg minr_(i < i0 | i \in A) F]
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]") : form_scope.

Notation "[ 'arg' 'minr_' ( i < i0 ) F ]" := [arg minr_(i < i0 | true) F]
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'minr_' ( i < i0 ) F ]") : form_scope.

Notation "[ 'arg' 'maxr_' ( i > i0 | P ) F ]" :=
     (arg_maxr i0 (fun i ⇒ P%B) (fun i ⇒ F))
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'maxr_' ( i > i0 | P ) F ]") : form_scope.

Notation "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]" :=
    [arg maxr_(i > i0 | i \in A) F]
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]") : form_scope.

Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F]
  (at level 0, i, i0 at level 10,
   format "[ 'arg' 'maxr_' ( i > i0 ) F ]") : form_scope.

Section RealDomainOperations.

sgr section

Variable R : realDomainType.
Implicit Types x y z t : R.
Hint Resolve (@num_real R) : core.

Lemma sgr_cp0 x :
  ((sg x == 1) = (0 < x)) ×
  ((sg x == -1) = (x < 0)) ×
  ((sg x == 0) = (x == 0)).

Variant sgr_val x : R → bool → bool → bool → bool → bool → bool
  → bool → bool → bool → bool → bool → bool → R → Set :=
  | SgrNull of x = 0 : sgr_val x 0 true true true true false false
    true false false true false false 0
  | SgrPos of x > 0 : sgr_val x x false false true false false true
    false false true false false true 1
  | SgrNeg of x < 0 : sgr_val x (- x) false true false false true false
    false true false false true false (-1).

Lemma sgrP x :
  sgr_val x `|x| (0 == x) (x ≤ 0) (0 ≤ x) (x == 0) (x < 0) (0 < x)
                 (0 == sg x) (-1 == sg x) (1 == sg x)
                 (sg x == 0) (sg x == -1) (sg x == 1) (sg x).

Lemma normrEsg x : `|x| = sg x × x.

Lemma numEsg x : x = sg x × `|x|.

GG: duplicate!
Lemma mulr_sg_norm x : sg x × `|x| = x.

Lemma sgrM x y : sg (x × y) = sg x × sg y.

Lemma sgrN x : sg (- x) = - sg x.

Lemma sgrX n x : sg (x ^+ n) = (sg x) ^+ n.

Lemma sgr_smul x y : sg (sg x × y) = sg x × sg y.

Lemma sgr_gt0 x : (sg x > 0) = (x > 0).

Lemma sgr_ge0 x : (sgr x ≥ 0) = (x ≥ 0).

norm section

Lemma ler_norm x : (x ≤ `|x|).

Lemma ler_norml x y : (`|x| ≤ y) = (- y ≤ x ≤ y).

Lemma ler_normlP x y : reflect ((- x ≤ y) × (x ≤ y)) (`|x| ≤ y).

Lemma eqr_norml x y : (`|x| == y) = ((x == y) || (x == -y)) && (0 ≤ y).

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

Lemma ltr_norml x y : (`|x| < y) = (- y < x < y).

Definition lter_norml := (ler_norml, ltr_norml).

Lemma ltr_normlP x y : reflect ((-x < y) × (x < y)) (`|x| < y).

Lemma ler_normr x y : (x ≤ `|y|) = (x ≤ y) || (x ≤ - y).

Lemma ltr_normr x y : (x < `|y|) = (x < y) || (x < - y).

Definition lter_normr := (ler_normr, ltr_normr).

Lemma ler_distl x y e : (`|x - y| ≤ e) = (y - e ≤ x ≤ y + e).

Lemma ltr_distl x y e : (`|x - y| < e) = (y - e < x < y + e).

Definition lter_distl := (ler_distl, ltr_distl).

Lemma exprn_even_ge0 n x : ~~ odd n → 0 ≤ x ^+ n.

Lemma exprn_even_gt0 n x : ~~ odd n → (0 < x ^+ n) = (n == 0)%N || (x != 0).

Lemma exprn_even_le0 n x : ~~ odd n → (x ^+ n ≤ 0) = (n != 0%N) && (x == 0).

Lemma exprn_even_lt0 n x : ~~ odd n → (x ^+ n < 0) = false.

Lemma exprn_odd_ge0 n x : odd n → (0 ≤ x ^+ n) = (0 ≤ x).

Lemma exprn_odd_gt0 n x : odd n → (0 < x ^+ n) = (0 < x).

Lemma exprn_odd_le0 n x : odd n → (x ^+ n ≤ 0) = (x ≤ 0).

Lemma exprn_odd_lt0 n x : odd n → (x ^+ n < 0) = (x < 0).

Special lemmas for squares.

Lemma sqr_ge0 x : 0 ≤ x ^+ 2.

Lemma sqr_norm_eq1 x : (x ^+ 2 == 1) = (`|x| == 1).

Lemma lerif_mean_square_scaled x y :
  x × y *+ 2 ≤ x ^+ 2 + y ^+ 2 ?= iff (x == y).

Lemma lerif_AGM2_scaled x y : x × y *+ 4 ≤ (x + y) ^+ 2 ?= iff (x == y).

Section MinMax.

GG: Many of the first lemmas hold unconditionally, and others hold for the real subset of a general domain.
Lemma minrC : @commutative R R min.

Lemma minrr : @idempotent R min.

Lemma minr_l x y : x ≤ y → min x y = x.

Lemma minr_r x y : y ≤ x → min x y = y.

Lemma maxrC : @commutative R R max.

Lemma maxrr : @idempotent R max.

Lemma maxr_l x y : y ≤ x → max x y = x.

Lemma maxr_r x y : x ≤ y → max x y = y.

Lemma addr_min_max x y : min x y + max x y = x + y.

Lemma addr_max_min x y : max x y + min x y = x + y.

Lemma minr_to_max x y : min x y = x + y - max x y.

Lemma maxr_to_min x y : max x y = x + y - min x y.

Lemma minrA x y z : min x (min y z) = min (min x y) z.

Lemma minrCA : @left_commutative R R min.

Lemma minrAC : @right_commutative R R min.

Variant minr_spec x y : bool → bool → R → Type :=
| Minr_r of x ≤ y : minr_spec x y true false x
| Minr_l of y < x : minr_spec x y false true y.

Lemma minrP x y : minr_spec x y (x ≤ y) (y < x) (min x y).

Lemma oppr_max x y : - max x y = min (- x) (- y).

Lemma oppr_min x y : - min x y = max (- x) (- y).

Lemma maxrA x y z : max x (max y z) = max (max x y) z.

Lemma maxrCA : @left_commutative R R max.

Lemma maxrAC : @right_commutative R R max.

Variant maxr_spec x y : bool → bool → R → Type :=
| Maxr_r of y ≤ x : maxr_spec x y true false x
| Maxr_l of x < y : maxr_spec x y false true y.

Lemma maxrP x y : maxr_spec x y (y ≤ x) (x < y) (maxr x y).

Lemma eqr_minl x y : (min x y == x) = (x ≤ y).

Lemma eqr_minr x y : (min x y == y) = (y ≤ x).

Lemma eqr_maxl x y : (max x y == x) = (y ≤ x).

Lemma eqr_maxr x y : (max x y == y) = (x ≤ y).

Lemma ler_minr x y z : (x ≤ min y z) = (x ≤ y) && (x ≤ z).

Lemma ler_minl x y z : (min y z ≤ x) = (y ≤ x) || (z ≤ x).

Lemma ler_maxr x y z : (x ≤ max y z) = (x ≤ y) || (x ≤ z).

Lemma ler_maxl x y z : (max y z ≤ x) = (y ≤ x) && (z ≤ x).

Lemma ltr_minr x y z : (x < min y z) = (x < y) && (x < z).

Lemma ltr_minl x y z : (min y z < x) = (y < x) || (z < x).

Lemma ltr_maxr x y z : (x < max y z) = (x < y) || (x < z).

Lemma ltr_maxl x y z : (max y z < x) = (y < x) && (z < x).

Definition lter_minr := (ler_minr, ltr_minr).
Definition lter_minl := (ler_minl, ltr_minl).
Definition lter_maxr := (ler_maxr, ltr_maxr).
Definition lter_maxl := (ler_maxl, ltr_maxl).

Lemma addr_minl : @left_distributive R R +%R min.

Lemma addr_minr : @right_distributive R R +%R min.

Lemma addr_maxl : @left_distributive R R +%R max.

Lemma addr_maxr : @right_distributive R R +%R max.

Lemma minrK x y : max (min x y) x = x.

Lemma minKr x y : min y (max x y) = y.

Lemma maxr_minl : @left_distributive R R max min.

Lemma maxr_minr : @right_distributive R R max min.

Lemma minr_maxl : @left_distributive R R min max.

Lemma minr_maxr : @right_distributive R R min max.

Lemma minr_pmulr x y z : 0 ≤ x → x × min y z = min (x × y) (x × z).

Lemma minr_nmulr x y z : x ≤ 0 → x × min y z = max (x × y) (x × z).

Lemma maxr_pmulr x y z : 0 ≤ x → x × max y z = max (x × y) (x × z).

Lemma maxr_nmulr x y z : x ≤ 0 → x × max y z = min (x × y) (x × z).

Lemma minr_pmull x y z : 0 ≤ x → min y z × x = min (y × x) (z × x).

Lemma minr_nmull x y z : x ≤ 0 → min y z × x = max (y × x) (z × x).

Lemma maxr_pmull x y z : 0 ≤ x → max y z × x = max (y × x) (z × x).

Lemma maxr_nmull x y z : x ≤ 0 → max y z × x = min (y × x) (z × x).

Lemma maxrN x : max x (- x) = `|x|.

Lemma maxNr x : max (- x) x = `|x|.

Lemma minrN x : min x (- x) = - `|x|.

Lemma minNr x : min (- x) x = - `|x|.

End MinMax.

Section PolyBounds.

Variable p : {poly R}.

Lemma poly_itv_bound a b : {ub | ∀ x, a ≤ x ≤ b → `|p.[x]| ≤ ub}.

Lemma monic_Cauchy_bound : p \is monic → {b | ∀ x, x ≥ b → p.[x] > 0}.

End PolyBounds.

End RealDomainOperations.

Section RealField.

Variables (F : realFieldType) (x y : F).

Lemma lerif_mean_square : x × y ≤ (x ^+ 2 + y ^+ 2) / 2%:R ?= iff (x == y).

Lemma lerif_AGM2 : x × y ≤ ((x + y) / 2%:R)^+ 2 ?= iff (x == y).

End RealField.

Section ArchimedeanFieldTheory.

Variables (F : archiFieldType) (x : F).

Lemma archi_boundP : 0 ≤ x → x < (bound x)%:R.

Lemma upper_nthrootP i : (bound x ≤ i)%N → x < 2%:R ^+ i.

End ArchimedeanFieldTheory.

Section RealClosedFieldTheory.

Variable R : rcfType.
Implicit Types a x y : R.

Lemma poly_ivt : real_closed_axiom R.

Square Root theory

Lemma sqrtr_ge0 a : 0 ≤ sqrt a.
Hint Resolve sqrtr_ge0 : core.

Lemma sqr_sqrtr a : 0 ≤ a → sqrt a ^+ 2 = a.

Lemma ler0_sqrtr a : a ≤ 0 → sqrt a = 0.

Lemma ltr0_sqrtr a : a < 0 → sqrt a = 0.

Variant sqrtr_spec a : R → bool → bool → R → Type :=
| IsNoSqrtr of a < 0 : sqrtr_spec a a false true 0
| IsSqrtr b of 0 ≤ b : sqrtr_spec a (b ^+ 2) true false b.

Lemma sqrtrP a : sqrtr_spec a a (0 ≤ a) (a < 0) (sqrt a).

Lemma sqrtr_sqr a : sqrt (a ^+ 2) = `|a|.

Lemma sqrtrM a b : 0 ≤ a → sqrt (a × b) = sqrt a × sqrt b.

Lemma sqrtr0 : sqrt 0 = 0 :> R.

Lemma sqrtr1 : sqrt 1 = 1 :> R.

Lemma sqrtr_eq0 a : (sqrt a == 0) = (a ≤ 0).

Lemma sqrtr_gt0 a : (0 < sqrt a) = (0 < a).

Lemma eqr_sqrt a b : 0 ≤ a → 0 ≤ b → (sqrt a == sqrt b) = (a == b).

Lemma ler_wsqrtr : {homo @sqrt R : a b / a ≤ b}.

Lemma ler_psqrt : {in @pos R &, {mono sqrt : a b / a ≤ b}}.

Lemma ler_sqrt a b : 0 < b → (sqrt a ≤ sqrt b) = (a ≤ b).

Lemma ltr_sqrt a b : 0 < b → (sqrt a < sqrt b) = (a < b).

End RealClosedFieldTheory.

Definition conjC {C : numClosedFieldType} : {rmorphism C → C} :=
 ClosedField.conj_op (ClosedField.conj_mixin (ClosedField.class C)).
Notation "z ^*" := (@conjC _ z) (at level 2, format "z ^*") : ring_scope.

Definition imaginaryC {C : numClosedFieldType} : C :=
 ClosedField.imaginary (ClosedField.conj_mixin (ClosedField.class C)).
Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope.

Section ClosedFieldTheory.

Variable C : numClosedFieldType.
Implicit Types a x y z : C.

Definition normCK x : `|x| ^+ 2 = x × x^*.

Lemma sqrCi : 'i ^+ 2 = -1 :> C.

Lemma conjCK : involutive (@conjC C).

Let Re2 z := z + z^*.
Definition nnegIm z := (0 ≤ imaginaryC × (z^* - z)).
Definition argCle y z := nnegIm z ==> nnegIm y && (Re2 z ≤ Re2 y).

Variant rootC_spec n (x : C) : Type :=
  RootCspec (y : C) of if (n > 0)%N then y ^+ n = x else y = 0
                        & ∀ z, (n > 0)%N → z ^+ n = x → argCle y z.

Fact rootC_subproof n x : rootC_spec n x.

Definition nthroot n x := let: RootCspec y _ _ := rootC_subproof n x in y.
Notation "n .-root" := (nthroot n) (at level 2, format "n .-root") : ring_scope.
Notation "n .-root" := (nthroot n) (only parsing) : ring_scope.
Notation sqrtC := 2.-root.

Definition Re x := (x + x^*) / 2%:R.
Definition Im x := 'i × (x^* - x) / 2%:R.
Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope.
Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope.

Let nz2 : 2%:R != 0 :> C.

Lemma normCKC x : `|x| ^+ 2 = x^* × x.

Lemma mul_conjC_ge0 x : 0 ≤ x × x^*.

Lemma mul_conjC_gt0 x : (0 < x × x^*) = (x != 0).

Lemma mul_conjC_eq0 x : (x × x^* == 0) = (x == 0).

Lemma conjC_ge0 x : (0 ≤ x^*) = (0 ≤ x).

Lemma conjC_nat n : (n%:R)^* = n%:R :> C.
Lemma conjC0 : 0^* = 0 :> C.
Lemma conjC1 : 1^* = 1 :> C.
Lemma conjC_eq0 x : (x^* == 0) = (x == 0).

Lemma invC_norm x : x^-1 = `|x| ^- 2 × x^*.

Real number subset.

Lemma CrealE x : (x \is real) = (x^* == x).

Lemma CrealP {x} : reflect (x^* = x) (x \is real).

Lemma conj_Creal x : x \is real → x^* = x.

Lemma conj_normC z : `|z|^* = `|z|.

Lemma geC0_conj x : 0 ≤ x → x^* = x.

Lemma geC0_unit_exp x n : 0 ≤ x → (x ^+ n.+1 == 1) = (x == 1).

Elementary properties of roots.

Ltac case_rootC := rewrite /nthroot; case: (rootC_subproof _ _).

Lemma root0C x : 0.-root x = 0.

Lemma rootCK n : (n > 0)%N → cancel n.-root (fun x ⇒ x ^+ n).

Lemma root1C x : 1.-root x = x.

Lemma rootC0 n : n.-root 0 = 0.

Lemma rootC_inj n : (n > 0)%N → injective n.-root.

Lemma eqr_rootC n : (n > 0)%N → {mono n.-root : x y / x == y}.

Lemma rootC_eq0 n x : (n > 0)%N → (n.-root x == 0) = (x == 0).

Rectangular coordinates.

Lemma nonRealCi : ('i : C) \isn't real.

Lemma neq0Ci : 'i != 0 :> C.

Lemma normCi : `|'i| = 1 :> C.

Lemma invCi : 'i^-1 = - 'i :> C.

Lemma conjCi : 'i^* = - 'i :> C.

Lemma Crect x : x = 'Re x + 'i × 'Im x.

Lemma Creal_Re x : 'Re x \is real.

Lemma Creal_Im x : 'Im x \is real.
Hint Resolve Creal_Re Creal_Im : core.

Fact Re_is_additive : additive Re.
Canonical Re_additive := Additive Re_is_additive.

Fact Im_is_additive : additive Im.
Canonical Im_additive := Additive Im_is_additive.

Lemma Creal_ImP z : reflect ('Im z = 0) (z \is real).

Lemma Creal_ReP z : reflect ('Re z = z) (z \in real).

Lemma ReMl : {in real, ∀ x, {morph Re : z / x × z}}.

Lemma ReMr : {in real, ∀ x, {morph Re : z / z × x}}.

Lemma ImMl : {in real, ∀ x, {morph Im : z / x × z}}.

Lemma ImMr : {in real, ∀ x, {morph Im : z / z × x}}.

Lemma Re_i : 'Re 'i = 0.

Lemma Im_i : 'Im 'i = 1.

Lemma Re_conj z : 'Re z^* = 'Re z.

Lemma Im_conj z : 'Im z^* = - 'Im z.

Lemma Re_rect : {in real &, ∀ x y, 'Re (x + 'i × y) = x}.

Lemma Im_rect : {in real &, ∀ x y, 'Im (x + 'i × y) = y}.

Lemma conjC_rect : {in real &, ∀ x y, (x + 'i × y)^* = x - 'i × y}.

Lemma addC_rect x1 y1 x2 y2 :
  (x1 + 'i × y1) + (x2 + 'i × y2) = x1 + x2 + 'i × (y1 + y2).

Lemma oppC_rect x y : - (x + 'i × y) = - x + 'i × (- y).

Lemma subC_rect x1 y1 x2 y2 :
  (x1 + 'i × y1) - (x2 + 'i × y2) = x1 - x2 + 'i × (y1 - y2).

Lemma mulC_rect x1 y1 x2 y2 :
  (x1 + 'i × y1) × (x2 + 'i × y2)
      = x1 × x2 - y1 × y2 + 'i × (x1 × y2 + x2 × y1).

Lemma normC2_rect :
  {in real &, ∀ x y, `|x + 'i × y| ^+ 2 = x ^+ 2 + y ^+ 2}.

Lemma normC2_Re_Im z : `|z| ^+ 2 = 'Re z ^+ 2 + 'Im z ^+ 2.

Lemma invC_rect :
  {in real &, ∀ x y, (x + 'i × y)^-1 = (x - 'i × y) / (x ^+ 2 + y ^+ 2)}.

Lemma lerif_normC_Re_Creal z : `|'Re z| ≤ `|z| ?= iff (z \is real).

Lemma lerif_Re_Creal z : 'Re z ≤ `|z| ?= iff (0 ≤ z).

Equality from polar coordinates, for the upper plane.
Lemma eqC_semipolar x y :
  `|x| = `|y| → 'Re x = 'Re y → 0 ≤ 'Im x × 'Im y → x = y.

Nth roots.

Let argCleP y z :
  reflect (0 ≤ 'Im z → 0 ≤ 'Im y ∧ 'Re z ≤ 'Re y) (argCle y z).
case Du: sqrCi => [u u2N1] /=. have/eqP := u2N1; rewrite -sqrCi eqf_sqr => /pred2P[ ] //. have:= conjCi; rewrite /'i; case_rootC => /= v v2n1 min_v conj_v Duv. have{min_v} /idPn[ ] := min_v u isT u2N1; rewrite negb_imply /nnegIm Du /= Duv. rewrite rmorphN conj_v opprK -opprD mulrNN mulNr -mulr2n mulrnAr -expr2 v2n1. by rewrite mulNrn opprK ler0n oppr_ge0 (ler_nat _ 2 0).

Lemma rootC_Re_max n x y :
  (n > 0)%N → y ^+ n = x → 0 ≤ 'Im y → 'Re y ≤ 'Re (n.-root x).

Let neg_unity_root n : (n > 1)%N → exists2 w : C, w ^+ n = 1 & 'Re w < 0.

Lemma Im_rootC_ge0 n x : (n > 1)%N → 0 ≤ 'Im (n.-root x).

Lemma rootC_lt0 n x : (1 < n)%N → (n.-root x < 0) = false.

Lemma rootC_ge0 n x : (n > 0)%N → (0 ≤ n.-root x) = (0 ≤ x).

Lemma rootC_gt0 n x : (n > 0)%N → (n.-root x > 0) = (x > 0).

Lemma rootC_le0 n x : (1 < n)%N → (n.-root x ≤ 0) = (x == 0).

Lemma ler_rootCl n : (n > 0)%N → {in Num.nneg, {mono n.-root : x y / x ≤ y}}.

Lemma ler_rootC n : (n > 0)%N → {in Num.nneg &, {mono n.-root : x y / x ≤ y}}.

Lemma ltr_rootCl n : (n > 0)%N → {in Num.nneg, {mono n.-root : x y / x < y}}.

Lemma ltr_rootC n : (n > 0)%N → {in Num.nneg &, {mono n.-root : x y / x < y}}.

Lemma exprCK n x : (0 < n)%N → 0 ≤ x → n.-root (x ^+ n) = x.

Lemma norm_rootC n x : `|n.-root x| = n.-root `|x|.

Lemma rootCX n x k : (n > 0)%N → 0 ≤ x → n.-root (x ^+ k) = n.-root x ^+ k.

Lemma rootC1 n : (n > 0)%N → n.-root 1 = 1.

Lemma rootCpX n x k : (k > 0)%N → 0 ≤ x → n.-root (x ^+ k) = n.-root x ^+ k.

Lemma rootCV n x : (n > 0)%N → 0 ≤ x → n.-root x^-1 = (n.-root x)^-1.

Lemma rootC_eq1 n x : (n > 0)%N → (n.-root x == 1) = (x == 1).

Lemma rootC_ge1 n x : (n > 0)%N → (n.-root x ≥ 1) = (x ≥ 1).

Lemma rootC_gt1 n x : (n > 0)%N → (n.-root x > 1) = (x > 1).

Lemma rootC_le1 n x : (n > 0)%N → 0 ≤ x → (n.-root x ≤ 1) = (x ≤ 1).

Lemma rootC_lt1 n x : (n > 0)%N → 0 ≤ x → (n.-root x < 1) = (x < 1).

Lemma rootCMl n x z : 0 ≤ x → n.-root (x × z) = n.-root x × n.-root z.

Lemma rootCMr n x z : 0 ≤ x → n.-root (z × x) = n.-root z × n.-root x.

Lemma imaginaryCE : 'i = sqrtC (-1).

More properties of n.-root will be established in cyclotomic.v.
The proper form of the Arithmetic - Geometric Mean inequality.

Lemma lerif_rootC_AGM (I : finType) (A : {pred I}) (n := #|A|) E :
    {in A, ∀ i, 0 ≤ E i} →
  n.-root (\prod_(i in A) E i) ≤ (\sum_(i in A) E i) / n%:R
                             ?= iff [∀ i in A, ∀ j in A, E i == E j].

Square root.

Lemma sqrtC0 : sqrtC 0 = 0.
Lemma sqrtC1 : sqrtC 1 = 1.
Lemma sqrtCK x : sqrtC x ^+ 2 = x.
Lemma sqrCK x : 0 ≤ x → sqrtC (x ^+ 2) = x.

Lemma sqrtC_ge0 x : (0 ≤ sqrtC x) = (0 ≤ x).
Lemma sqrtC_eq0 x : (sqrtC x == 0) = (x == 0).
Lemma sqrtC_gt0 x : (sqrtC x > 0) = (x > 0).
Lemma sqrtC_lt0 x : (sqrtC x < 0) = false.
Lemma sqrtC_le0 x : (sqrtC x ≤ 0) = (x == 0).

Lemma ler_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x ≤ y}}.
Lemma ltr_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x < y}}.
Lemma eqr_sqrtC : {mono sqrtC : x y / x == y}.
Lemma sqrtC_inj : injective sqrtC.
Lemma sqrtCM : {in Num.nneg &, {morph sqrtC : x y / x × y}}.

Lemma sqrCK_P x : reflect (sqrtC (x ^+ 2) = x) ((0 ≤ 'Im x) && ~~ (x < 0)).

Lemma normC_def x : `|x| = sqrtC (x × x^*).

Lemma norm_conjC x : `|x^*| = `|x|.

Lemma normC_rect :
  {in real &, ∀ x y, `|x + 'i × y| = sqrtC (x ^+ 2 + y ^+ 2)}.

Lemma normC_Re_Im z : `|z| = sqrtC ('Re z ^+ 2 + 'Im z ^+ 2).

Norm sum (in)equalities.

Lemma normC_add_eq x y :
    `|x + y| = `|x| + `|y| →
  {t : C | `|t| == 1 & (x, y) = (`|x| × t, `|y| × t)}.

Lemma normC_sum_eq (I : finType) (P : pred I) (F : I → C) :
     `|\sum_(i | P i) F i| = \sum_(i | P i) `|F i| →
   {t : C | `|t| == 1 & ∀ i, P i → F i = `|F i| × t}.

Lemma normC_sum_eq1 (I : finType) (P : pred I) (F : I → C) :
    `|\sum_(i | P i) F i| = (\sum_(i | P i) `|F i|) →
     (∀ i, P i → `|F i| = 1) →
   {t : C | `|t| == 1 & ∀ i, P i → F i = t}.

Lemma normC_sum_upper (I : finType) (P : pred I) (F G : I → C) :
     (∀ i, P i → `|F i| ≤ G i) →
     \sum_(i | P i) F i = \sum_(i | P i) G i →
   ∀ i, P i → F i = G i.

Lemma normC_sub_eq x y :
  `|x - y| = `|x| - `|y| → {t | `|t| == 1 & (x, y) = (`|x| × t, `|y| × t)}.

End ClosedFieldTheory.

Notation "n .-root" := (@nthroot _ n)
  (at level 2, format "n .-root") : ring_scope.
Notation sqrtC := 2.-root.
Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope.
Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope.
Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope.


End Theory.

Module RealMixin.

Section RealMixins.

Variables (R : idomainType) (le : rel R) (lt : rel R) (norm : R → R).

Section LeMixin.

Hypothesis le0_add : ∀ x y, 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
Hypothesis le0_mul : ∀ x y, 0 ≤ x → 0 ≤ y → 0 ≤ x × y.
Hypothesis le0_anti : ∀ x, 0 ≤ x → x ≤ 0 → x = 0.
Hypothesis sub_ge0 : ∀ x y, (0 ≤ y - x) = (x ≤ y).
Hypothesis le0_total : ∀ x, (0 ≤ x) || (x ≤ 0).
Hypothesis normN: ∀ x, `|- x| = `|x|.
Hypothesis ge0_norm : ∀ x, 0 ≤ x → `|x| = x.
Hypothesis lt_def : ∀ x y, (x < y) = (y != x) && (x ≤ y).

Let le0N x : (0 ≤ - x) = (x ≤ 0).
Let leN_total x : 0 ≤ x ∨ 0 ≤ - x.

Let le00 : (0 ≤ 0).
Let le01 : (0 ≤ 1).

Fact lt0_add x y : 0 < x → 0 < y → 0 < x + y.

Fact eq0_norm x : `|x| = 0 → x = 0.

Fact le_def x y : (x ≤ y) = (`|y - x| == y - x).

Fact normM : {morph norm : x y / x × y}.

Fact le_normD x y : `|x + y| ≤ `|x| + `|y|.

Lemma le_total x y : (x ≤ y) || (y ≤ x).

Definition Le :=
  Mixin le_normD lt0_add eq0_norm (in2W le_total) normM le_def lt_def.

Lemma Real (R' : numDomainType) & phant R' :
  R' = NumDomainType R Le → real_axiom R'.

End LeMixin.

Section LtMixin.

Hypothesis lt0_add : ∀ x y, 0 < x → 0 < y → 0 < x + y.
Hypothesis lt0_mul : ∀ x y, 0 < x → 0 < y → 0 < x × y.
Hypothesis lt0_ngt0 : ∀ x, 0 < x → ~~ (x < 0).
Hypothesis sub_gt0 : ∀ x y, (0 < y - x) = (x < y).
Hypothesis lt0_total : ∀ x, x != 0 → (0 < x) || (x < 0).
Hypothesis normN : ∀ x, `|- x| = `|x|.
Hypothesis ge0_norm : ∀ x, 0 ≤ x → `|x| = x.
Hypothesis le_def : ∀ x y, (x ≤ y) = (y == x) || (x < y).

Fact le0_add x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.

Fact le0_mul x y : 0 ≤ x → 0 ≤ y → 0 ≤ x × y.

Fact le0_anti x : 0 ≤ x → x ≤ 0 → x = 0.

Fact sub_ge0 x y : (0 ≤ y - x) = (x ≤ y).

Fact lt_def x y : (x < y) = (y != x) && (x ≤ y).

Fact le0_total x : (0 ≤ x) || (x ≤ 0).

Definition Lt :=
  Le le0_add le0_mul le0_anti sub_ge0 le0_total normN ge0_norm lt_def.

End LtMixin.

End RealMixins.

End RealMixin.

End Num.

Export Num.NumDomain.Exports Num.NumField.Exports Num.ClosedField.Exports.
Export Num.RealDomain.Exports Num.RealField.Exports.
Export Num.ArchimedeanField.Exports Num.RealClosedField.Exports.
Export Num.Syntax Num.PredInstances.

Notation RealLeMixin := Num.RealMixin.Le.
Notation RealLtMixin := Num.RealMixin.Lt.
Notation RealLeAxiom R := (Num.RealMixin.Real (Phant R) (erefl _)).
Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin.