Library mathcomp.algebra.ssrnum

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

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

NumDomain (Integral domain with an order and a norm)

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

NumField (Field with an order and a norm)

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

NumClosedField (Closed Field with an order and a norm)

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

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

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

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

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

ArchiField (A Real Field with the archimedean axiom)

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

RealClosedField (Real Field with the real closed axiom)

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

Over these structures, we have the following operations `|x| == norm of x. x <= y <=> x is less than or equal to y (:= '|y - x| == y - x). x < y <=> x is less than y (:= (x <= y) && (x != y)). x <= y ?= iff C <-> x is less than y, or equal iff C is true. Num.sg x == sign of x: equal to 0 iff x = 0, to 1 iff x > 0, and to -1 in all other cases (including x < 0). x \is a Num.pos <=> x is positive (:= x > 0). x \is a Num.neg <=> x is negative (:= x < 0). x \is a Num.nneg <=> x is positive or 0 (:= x >= 0). x \is a Num.real <=> x is real (:= x >= 0 or x < 0). Num.min x y == minimum of x y Num.max x y == maximum of x y Num.bound x == in archimedean fields, and upper bound for x, i.e., and n such that `|x| < n%:R. Num.sqrt x == in a real-closed field, a positive square root of x if x >= 0, or 0 otherwise.

There are now three distinct uses of the symbols <, <=, > and >=: 0-ary, unary (prefix) and binary (infix). 0. <%R, <=%R, >%R, >=%R stand respectively for lt, le, gt and ge. 1. (< x), (<= x), (> x), (>= x) stand respectively for (gt x), (ge x), (lt x), (le x). So (< x) is a predicate characterizing elements smaller than x. 2. (x < y), (x <= y), ... mean what they are expected to. These convention are compatible with haskell's, where ((< y) x) = (x < y) = ((<) x y), except that we write <%R instead of (<).

list of prefixes : p : positive n : negative sp : strictly positive sn : strictly negative i : interior = in [0, 1] or ]0, 1[ e : exterior = in [1, +oo[ or ]1; +oo[ w : non strict (weak) monotony

Set Implicit Arguments.

Local Open Scope ring_scope.
Import GRing.Theory.

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

Module Num.

Principal mixin; further classes add axioms rather than operations.

Record mixin_of (R : ringType) := Mixin {
  norm_op : R → R;
  le_op : rel R;
  lt_op : rel R;
  _ : ∀ x y, le_op (norm_op (x + y)) (norm_op x + norm_op y);
  _ : ∀ x y, lt_op 0 x → lt_op 0 y → lt_op 0 (x + y);
  _ : ∀ x, norm_op x = 0 → x = 0;
  _ : ∀ x y, le_op 0 x → le_op 0 y → le_op x y || le_op y x;
  _ : {morph norm_op : x y / x × y};
  _ : ∀ x y, (le_op x y ) = (norm_op (y - x) == y - x );
  _ : ∀ x y, (lt_op x y ) = (y != x ) && (le_op x y )
}.

Base interface.

Module NumDomain.

Section ClassDef.

Record class_of T := Class {
  base : GRing.IntegralDomain.class_of T;
  mixin : mixin_of (ring_for T base)
}.
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (ring_for T b0)) :=
  fun bT b & phant_id (GRing.IntegralDomain.class bT) b ⇒
  fun m & phant_id m0 m ⇒ Pack (@Class T b m) T.

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

End ClassDef.

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

End NumDomain.
Import NumDomain.Exports.

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

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

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

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

Shorter qualified names, when Num.Def is not imported.

Notation norm := normr.
Notation le := ler.
Notation lt := ltr.
Notation ge := ger.
Notation gt := gtr.
Notation sg := sgr.
Notation max := maxr.
Notation min := minr.
Notation pos := Rpos.
Notation neg := Rneg.
Notation nneg := Rnneg.
Notation real := Rreal.

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

(Exported) symbolic syntax.

Module Import Syntax.
Import Def Keys.

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

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

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

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

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

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

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

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

Coercion ler_of_leif : lerif >-> is_true.

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

End Syntax.

Section ExtensionAxioms.

Variable R : numDomainType.

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

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

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

End ExtensionAxioms.

The rest of the numbers interface hierarchy.

Module NumField.

Section ClassDef.

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

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack :=
  fun bT b & phant_id (GRing.Field.class bT) (b : GRing.Field.class_of T) ⇒
  fun mT m & phant_id (NumDomain.class mT) (@NumDomain.Class T b m) ⇒
  Pack (@Class T b m) T.

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

End ClassDef.

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

End NumField.
Import NumField.Exports.

Module ClosedField.

Section ClassDef.

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

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack :=
  fun bT b & phant_id (GRing.ClosedField.class bT)
                      (b : GRing.ClosedField.class_of T) ⇒
  fun mT m & phant_id (NumField.class mT) (@NumField.Class T b m) ⇒
  Pack (@Class T b m) T.

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

End ClassDef.

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

End ClosedField.
Import ClosedField.Exports.

Module RealDomain.

Section ClassDef.

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

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : real_axiom (num_for T b0)) :=
  fun bT b & phant_id (NumDomain.class bT) b ⇒
  fun m & phant_id m0 m ⇒ Pack (@Class T b m) T.

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

End ClassDef.

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

End RealDomain.
Import RealDomain.Exports.

Module RealField.

Section ClassDef.

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

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack :=
  fun bT b & phant_id (NumField.class bT) (b : NumField.class_of T) ⇒
  fun mT m & phant_id (RealDomain.class mT) (@RealDomain.Class T b m) ⇒
  Pack (@Class T b m) T.

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

End ClassDef.

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

End RealField.
Import RealField.Exports.

Module ArchimedeanField.

Section ClassDef.

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

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : archimedean_axiom (num_for T b0)) :=
  fun bT b & phant_id (RealField.class bT) b ⇒
  fun m & phant_id m0 m ⇒ Pack (@Class T b m) T.

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

End ClassDef.

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

End ArchimedeanField.
Import ArchimedeanField.Exports.

Module RealClosedField.

Section ClassDef.

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

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : real_closed_axiom (num_for T b0)) :=
  fun bT b & phant_id (RealField.class bT) b ⇒
  fun m & phant_id m0 m ⇒ Pack (@Class T b m) T.

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

End ClassDef.

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

End RealClosedField.
Import RealClosedField.Exports.

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

Module Import Internals.

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

Lemmas from the signature

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

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

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

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

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

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

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

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

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

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

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

Lemma ler01 : 0 ≤ 1 :> R.

Lemma ltr01 : 0 < 1 :> R.

Lemma ltrW x y : x < y → x ≤ y.

Lemma lerr x : x ≤ x.

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

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

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

Closure properties of the real predicates.

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

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

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

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

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

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

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

End Domain.

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

Fact archi_bound_subproof (R : archiFieldType) : archimedean_axiom R.

Section RealClosed.
Variable R : rcfType.

Lemma poly_ivt : real_closed_axiom R.

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

End RealClosed.

End Internals.

Module PredInstances.

Canonical pos_mulrPred.
Canonical pos_divrPred.

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

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

End PredInstances.

Module Import ExtraDef.

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

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

End ExtraDef.

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

Module Theory.

Section NumIntegralDomainTheory.

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

Lemmas from the signature (reexported from internals).

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

Predicate and relation definitions.

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

General properties of <= and <

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

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

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

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

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

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

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

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

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

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

Integer comparisons and characteristic 0.

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

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

Lemma char_num : [char R ] =i pred0.

Properties of the norm.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Comparision to 0 of a difference

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

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

Ordered ring properties.

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

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

Lemma ltr_trans : transitive (@ltr R).

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

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

Lemma ler_trans : transitive (@ler R).

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

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

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

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

Lemma ler_anti : antisymmetric (@ler R).

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

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

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

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

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

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

Norm and order properties.

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

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

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

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

End NumIntegralDomainTheory.

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

Section NumIntegralDomainMonotonyTheory.

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

Section AcrossTypes.

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

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

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

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

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

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

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

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

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

Monotony in D D'

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

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

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

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

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

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

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

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

End AcrossTypes.

Section NatToR.

Variable (f : nat → R).

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

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

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

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

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

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

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

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

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

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

End NatToR.

End NumIntegralDomainMonotonyTheory.

Section NumDomainOperationTheory.

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

Comparision and opposite.

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

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

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

Definition lter_oppr := (ler_oppr , ltr_oppr ).

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

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

Definition lter_oppl := (ler_oppl , ltr_oppl ).

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

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

Definition oppr_gte0 := (oppr_ge0 , oppr_gt0 ).

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

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

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

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

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

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

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

Properties of the real subset.

Lemma ger0_real x : 0 ≤ x → x \is real.

Lemma ler0_real x : x ≤ 0 → x \is real.

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

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

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

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

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

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

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

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

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

:TODO: add a rpredBC in ssralg

Lemma realBC x y : (x - y \is real ) = (y - x \is real ).

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

dichotomy and trichotomy

real wlog

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

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

Monotony of addition

Lemma ler_add2l x : {mono +%R x : y z / y ≤ z}.

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

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

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

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

Addition, subtraction and transitivity

Lemma ler_add x y z t : x ≤ y → z ≤ t → x + z ≤ y + t.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Addition with left member knwon to be positive/negative

Lemma ler_paddl y x z : 0 ≤ x → y ≤ z → y ≤ x + z.

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

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

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

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

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

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

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

Addition with right member we know positive/negative

Lemma ler_paddr y x z : 0 ≤ x → y ≤ z → y ≤ z + x.

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

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

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

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

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

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

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

x and y have the same sign and their sum is null

Lemma paddr_eq0 (x y : R) :
  0 ≤ x → 0 ≤ y → (x + y == 0) = (x == 0) && (y == 0).

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

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

big sum and ler

Lemma sumr_ge0 I (r : seq I) (P : pred I) (F : I → R) :
  (∀ i, P i → (0 ≤ F i )) → 0 ≤ \sum_(i <- r | P i) (F i).

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

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

:TODO: Cyril : See which form to keep

Lemma psumr_eq0P (I : finType) (P : pred I) (F : I → R) :
(∀ i, P i → 0 ≤ F i ) → \sum_(i | P i) F i = 0 →
(∀ i, P i → F i = 0).

mulr and ler/ltr

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

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

Definition lter_pmul2l := (ler_pmul2l , ltr_pmul2l ).

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

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

Definition lter_pmul2r := (ler_pmul2r , ltr_pmul2r ).

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

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

Definition lter_nmul2l := (ler_nmul2l , ltr_nmul2l ).

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

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

Definition lter_nmul2r := (ler_nmul2r , ltr_nmul2r ).

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

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

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

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

Binary forms, for backchaining.

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

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

complement for x *+ n and <= or <

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

More characteristic zero properties.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(x * y) compared to 0 Remark : pmulr_rgt0 and pmulr_rge0 are defined above

x positive and y right

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

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

x positive and y left

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

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

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

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

x negative and y right

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

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

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

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

x negative and y left

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

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

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

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

weak and symmetric lemmas

Lemma mulr_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x × y.

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

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

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

mulr_gt0 with only one case

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

Iterated products

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

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

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

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

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

real of mul

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

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

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

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

ler/ltr and multiplication between a positive/negative

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

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

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

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

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

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

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

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

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

Lemma gtr_nmull x y : y < 0 → (x × y < y ) = (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.

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).
Implicit Arguments real_ler_normlP [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).
Implicit Arguments real_ltr_normlP [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.
Implicit Arguments ler_sqr [[R] x y].
Implicit Arguments ltr_sqr [[R] x y].
Implicit Arguments signr_inj [[R] x1 x2].
Implicit Arguments real_ler_normlP [R x y].
Implicit Arguments real_ltr_normlP [R x y].
Implicit Arguments lerif_refl [R x C].
Implicit Arguments mono_in_lerif [R A f C].
Implicit Arguments nmono_in_lerif [R A f C].
Implicit Arguments mono_lerif [R f C].
Implicit Arguments nmono_lerif [R f C].

Section NumDomainMonotonyTheoryForReals.

Variables (R R' : numDomainType) (D : pred R) (f : R → R').
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}}.

GG: Domain should precede condition.

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

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.

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

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

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.

Section RealDomainMonotony.

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

Hint Resolve (@num_real R).

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

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

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

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

End RealDomainMonotony.

Section RealDomainOperations.

sgr section

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

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

CoInductive 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).
Implicit Arguments ler_normlP [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).
Implicit Arguments ltr_normlP [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.

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

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

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.

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

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