Library mathcomp.algebra.ssrnum

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

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import ssrAC div fintype path bigop order finset fingroup.
From mathcomp Require Import ssralg poly.

Number structures NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This file defines some classes to manipulate number structures, i.e, structures with an order and a norm. To use this file, insert "Import Num.Theory." before your scripts. You can also "Import Num.Def." to enjoy shorter notations (e.g., minr instead of Num.min, lerif instead of Num.leif, etc.). This file defines the following number structures: porderZmodType == join of Order.POrder and GRing.Zmodule The HB class is called POrderedZmodule. normedZmodType == Zmodule with a norm The HB class is called NormedZmodule. numDomainType == Integral domain with an order and a norm The HB class is called NumDomain. numFieldType == Field with an order and a norm The HB class is called NumField. numClosedFieldType == Partially ordered Closed Field with conjugation The HB class is called ClosedField. realDomainType == Num domain where all elements are positive or negative The HB class is called RealDomain. realFieldType == Num Field where all elements are positive or negative The HB class is called RealField. rcfType == A Real Field with the real closed axiom The HB class is called RealClosedField. The ordering symbols and notations (<, <=, >, >=, _ <= _ ?= iff _, _ < _ ?<= if _, >=<, and ><) and lattice operations (meet and join) defined in order.v are redefined for the ring_display in the ring_scope (%R). 0-ary ordering symbols for the ring_display have the suffix "%R", e.g., <%R. All the other ordering notations are the same as order.v. Over these structures, we have the following operations: `|x| == norm of x 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.npos <=> x is negative or 0 (:= x <= 0) x \is a Num.real <=> x is real (:= x >= 0 or x < 0) 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).
  • 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
Pdeg2.NumClosed : theory of the degree 2 polynomials on NumClosedField. Pdeg2.NumClosedMonic : theory of Pdeg2.NumClosed specialized to monic polynomials. Pdeg2.Real : theory of the degree 2 polynomials on RealField and rcfType. Pdeg2.RealMonic : theory of Pdeg2.Real specialized to monic polynomials.

Set Implicit Arguments.

Reserved Notation "n .-root" (at level 2, format "n .-root").
Reserved Notation "'i" (at level 0).
Reserved Notation "'Re z" (at level 10, z at level 8).
Reserved Notation "'Im z" (at level 10, z at level 8).

Local Open Scope order_scope.
Local Open Scope ring_scope.
Import Order.TTheory GRing.Theory.

Fact ring_display : unit.

Module Num.

#[short(type="porderZmodType")]
HB.structure Definition POrderedZmodule :=
  { R of Order.isPOrder ring_display R & GRing.Zmodule R }.


#[short(type="normedZmodType")]
HB.structure Definition NormedZmodule (R : porderZmodType) :=
  { M of Zmodule_isNormed R M & GRing.Zmodule M }.
Arguments norm {R M} x : rename.

Module NormedZmoduleExports.
Bind Scope ring_scope with NormedZmodule.sort.
Notation " [ 'normedZmodType' R 'of' T 'for' cT ]" := (@clone _ (Phant R) T cT _ idfun) (at level 0, format " [ 'normedZmodType' R 'of' T 'for' cT ]") : form_scope. Notation " [ 'normedZmodType' R 'of' T ]" := (@clone _ (Phant R) T _ _ id) (at level 0, format " [ 'normedZmodType' R 'of' T ]") : form_scope.
End NormedZmoduleExports.


#[short(type="numDomainType")]
HB.structure Definition NumDomain := { R of
     GRing.IntegralDomain R &
     POrderedZmodule R &
     NormedZmodule (POrderedZmodule.clone R _) R &
     isNumRing R
  }.
Arguments addr_gt0 {_} [x y] : rename.
Arguments ger_leVge {_} [x y] : rename.

TODO: make isNumDomain depend on intermediate structures TODO: make isNumDomain.sort canonically a NumDomain

Module NumDomainExports.
Bind Scope ring_scope with NumDomain.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use Num.NumDomain.clone instead.")]
Notation "[ 'numDomainType' 'of' T 'for' cT ]" := (NumDomain.clone T%type cT)
  (at level 0, format "[ 'numDomainType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Num.NumDomain.clone instead.")]
Notation "[ 'numDomainType' 'of' T ]" := (NumDomain.clone T%type _)
  (at level 0, format "[ 'numDomainType' 'of' T ]") : form_scope.
End NumDomainExports.


#[short(type="archiNumDomainType")]
HB.structure Definition ArchiNumDomain :=
  { R of NumDomain_isArchimedean R & NumDomain R }.

Module ArchiNumDomainExports.
Bind Scope ring_scope with ArchiNumDomain.sort.
#[deprecated(since="mathcomp 2.1.0", note="Require archimedean.v.")]
Notation archiNumDomainType := archiNumDomainType (only parsing).
End ArchiNumDomainExports.

Module Import Def.

Notation normr := norm.

Notation ler := (@Order.le ring_display _) (only parsing).
Notation "@ 'ler' R" := (@Order.le ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation ltr := (@Order.lt ring_display _) (only parsing).
Notation "@ 'ltr' R" := (@Order.lt ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation ger := (@Order.ge ring_display _) (only parsing).
Notation "@ 'ger' R" := (@Order.ge ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation gtr := (@Order.gt ring_display _) (only parsing).
Notation "@ 'gtr' R" := (@Order.gt ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation lerif := (@Order.leif ring_display _) (only parsing).
Notation "@ 'lerif' R" := (@Order.leif ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation lterif := (@Order.lteif ring_display _) (only parsing).
Notation "@ 'lteif' R" := (@Order.lteif ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation comparabler := (@Order.comparable ring_display _) (only parsing).
Notation "@ 'comparabler' R" := (@Order.comparable ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.
Notation maxr := (@Order.max ring_display _).
Notation "@ 'maxr' R" := (@Order.max ring_display R)
    (at level 10, R at level 8, only parsing) : fun_scope.
Notation minr := (@Order.min ring_display _).
Notation "@ 'minr' R" := (@Order.min ring_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.

Section NumDomainDef.
Context {R : numDomainType}.

Definition sgr (x : R) : R := if x == 0 then 0 else if x < 0 then -1 else 1.
Definition Rpos_pred := fun x : R ⇒ 0 < x.
Definition Rpos : qualifier 0 R := [qualify x | Rpos_pred x].
Definition Rneg_pred := fun x : Rx < 0.
Definition Rneg : qualifier 0 R := [qualify x : R | Rneg_pred x].
Definition Rnneg_pred := fun x : R ⇒ 0 x.
Definition Rnneg : qualifier 0 R := [qualify x : R | Rnneg_pred x].
Definition Rnpos_pred := fun x : Rx 0.
Definition Rnpos : qualifier 0 R := [qualify x : R | Rnpos_pred x].
Definition Rreal_pred := fun x : R(0 x) || (x 0).
Definition Rreal : qualifier 0 R := [qualify x : R | Rreal_pred x].

End NumDomainDef.

Section ArchiNumDomainDef.
Context {R : ArchiNumDomain.type}.

Definition trunc : R nat := @trunc_subdef R.
Definition nat_num : qualifier 1 R := [qualify a x : R | nat_num_subdef x].
Definition int_num : qualifier 1 R := [qualify a x : R | int_num_subdef x].

End ArchiNumDomainDef.

End Def.

Arguments Rpos_pred _ _ /.
Arguments Rneg_pred _ _ /.
Arguments Rnneg_pred _ _ /.
Arguments Rreal_pred _ _ /.

Arguments trunc {R} : simpl never.
Arguments nat_num {R} : simpl never.
Arguments int_num {R} : simpl never.

Shorter qualified names, when Num.Def is not imported.
Notation le := ler (only parsing).
Notation lt := ltr (only parsing).
Notation ge := ger (only parsing).
Notation gt := gtr (only parsing).
Notation leif := lerif (only parsing).
Notation lteif := lterif (only parsing).
Notation comparable := comparabler (only parsing).
Notation sg := sgr.
Notation max := maxr.
Notation min := minr.
Notation pos := Rpos.
Notation neg := Rneg.
Notation nneg := Rnneg.
Notation npos := Rnpos.
Notation real := Rreal.
Not to pollute the local namespace, Num.nat and Num.int are defined later.
#[deprecated(since="mathcomp 2.1.0", note="Require archimedean.v.")]
Notation trunc := trunc (only parsing).

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

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

Notation "<=%R" := le : fun_scope.
Notation ">=%R" := ge : fun_scope.
Notation "<%R" := lt : fun_scope.
Notation ">%R" := gt : fun_scope.
Notation "<?=%R" := leif : fun_scope.
Notation "<?<=%R" := lteif : fun_scope.
Notation ">=<%R" := comparable : fun_scope.
Notation "><%R" := (fun x y~~ (comparable x y)) : fun_scope.

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

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

Notation "x <= y" := (le x y) : ring_scope.
Notation "x <= y :> T" := ((x : T) (y : T)) (only parsing) : 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" := (lt x y) : ring_scope.
Notation "x < y :> T" := ((x : T) < (y : T)) (only parsing) : 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.

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

Notation ">=< y" := [pred x | comparable x y] : ring_scope.
Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : ring_scope.
Notation "x >=< y" := (comparable x y) : ring_scope.

Notation ">< y" := [pred x | ~~ comparable x y] : ring_scope.
Notation ">< y :> T" := (>< (y : T)) (only parsing) : ring_scope.
Notation "x >< y" := (~~ (comparable x y)) : ring_scope.

Export Order.POCoercions.

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.

#[short(type="numFieldType")]
HB.structure Definition NumField := { R of GRing.UnitRing_isField R &
     GRing.IntegralDomain R &
     POrderedZmodule R &
     NormedZmodule (POrderedZmodule.clone R _) R &
     isNumRing R }.

Module NumFieldExports.
Bind Scope ring_scope with NumField.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use Num.NumField.clone instead.")]
Notation "[ 'numFieldType' 'of' T ]" := (NumField.clone T%type _)
  (at level 0, format "[ 'numFieldType' 'of' T ]") : form_scope.
End NumFieldExports.


#[short(type="numClosedFieldType")]
HB.structure Definition ClosedField :=
  { R of NumField_isImaginary R & GRing.ClosedField R & NumField R }.

Module ClosedFieldExports.
Bind Scope ring_scope with ClosedField.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use Num.ClosedField.clone instead.")]
Notation "[ 'numClosedFieldType' 'of' T 'for' cT ]" := (ClosedField.clone T%type cT)
  (at level 0, format "[ 'numClosedFieldType' 'of' T 'for' cT ]") :
                                                         form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Num.ClosedField.clone instead.")]
Notation "[ 'numClosedFieldType' 'of' T ]" := (ClosedField.clone T%type _)
  (at level 0, format "[ 'numClosedFieldType' 'of' T ]") : form_scope.
End ClosedFieldExports.

#[short(type="realDomainType")]
HB.structure Definition RealDomain :=
  { R of Order.Total ring_display R & NumDomain R }.

Module RealDomainExports.
Bind Scope ring_scope with RealDomain.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use Num.RealDomain.clone instead.")]
Notation "[ 'realDomainType' 'of' T ]" := (RealDomain.clone T%type _)
  (at level 0, format "[ 'realDomainType' 'of' T ]") : form_scope.
End RealDomainExports.

#[short(type="realFieldType")]
HB.structure Definition RealField :=
  { R of Order.Total ring_display R & NumField R }.

Module RealFieldExports.
Bind Scope ring_scope with RealField.sort.
#[deprecated(since="mathcomp 2.0.0", note="Use Num.RealField.clone instead.")]
Notation "[ 'realFieldType' 'of' T ]" := (RealField.clone T%type _)
  (at level 0, format "[ 'realFieldType' 'of' T ]") : form_scope.
End RealFieldExports.


#[short(type="rcfType")]
HB.structure Definition RealClosedField :=
  { R of RealField_isClosed R & RealField R }.

Module RealClosedFieldExports.
Bind Scope ring_scope with RealClosedField.sort.
#[deprecated(since="mathcomp 2.0.0",
  note="Use Num.RealClosedField.clone instead.")]
Notation "[ 'rcfType' 'of' T 'for' cT ]" := (RealClosedField.clone T%type cT)
  (at level 0, format "[ 'rcfType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
  note="Use Num.RealClosedField.clone instead.")]
Notation "[ 'rcfType' 'of' T ]" := (RealClosedField.clone T%type _)
  (at level 0, format "[ 'rcfType' 'of' T ]") : form_scope.
End RealClosedFieldExports.

#[short(type="archiNumFieldType")]
HB.structure Definition ArchiNumField :=
  { R of NumDomain_isArchimedean R & NumField R }.

Module ArchiNumFieldExports.
Bind Scope ring_scope with ArchiNumField.sort.
#[deprecated(since="mathcomp 2.1.0", note="Require archimedean.v.")]
Notation archiNumFieldType := archiNumFieldType (only parsing).
End ArchiNumFieldExports.

#[short(type="archiClosedFieldType")]
HB.structure Definition ArchiClosedField :=
  { R of NumDomain_isArchimedean R & ClosedField R }.

Module ArchiClosedFieldExports.
Bind Scope ring_scope with ArchiClosedField.sort.
#[deprecated(since="mathcomp 2.1.0", note="Require archimedean.v.")]
Notation archiClosedFieldType := archiClosedFieldType (only parsing).
End ArchiClosedFieldExports.

#[short(type="archiDomainType")]
HB.structure Definition ArchiDomain :=
  { R of NumDomain_isArchimedean R & RealDomain R }.

Module ArchiDomainExports.
Bind Scope ring_scope with ArchiDomain.sort.
#[deprecated(since="mathcomp 2.1.0", note="Require archimedean.v.")]
Notation archiDomainType := archiDomainType (only parsing).
End ArchiDomainExports.

#[short(type="archiFieldType")]
HB.structure Definition ArchiField :=
  { R of NumDomain_isArchimedean R & RealField R }.

Module ArchiFieldExports.
Bind Scope ring_scope with ArchiField.sort.
#[deprecated(since="mathcomp 2.1.0", note="Require archimedean.v.")]
Notation archiFieldType := archiFieldType (only parsing).
#[deprecated(since="mathcomp 2.0.0",
  note="Use Num.ArchiField.clone instead.")]
Notation "[ 'archiFieldType' 'of' T 'for' cT ]" := (ArchiField.clone T%type cT)
  (at level 0, format "[ 'archiFieldType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0",
  note="Use Num.ArchiField.clone instead.")]
Notation "[ 'archiFieldType' 'of' T ]" := (ArchiField.clone T%type _)
  (at level 0, format "[ 'archiFieldType' 'of' T ]") : form_scope.
End ArchiFieldExports.

Module ArchimedeanField.
#[deprecated(since="mathcomp 2.1.0",
  note="Require archimedean.v and use archiFieldType instead.")]
Notation sort := ArchiField.sort (only parsing).
#[deprecated(since="mathcomp 2.1.0",
  note="Require archimedean.v and use archiFieldType.on instead.")]
Notation on R := (ArchiField.on R) (only parsing).
End ArchimedeanField.
#[deprecated(since="mathcomp 2.1.0",
  note="Require archimedean.v and use ArchiField instead.")]
Notation ArchimedeanField R := (ArchiField R) (only parsing).

#[short(type="archiRcfType")]
HB.structure Definition ArchiRealClosedField :=
  { R of NumDomain_isArchimedean R & RealClosedField R }.

Module ArchiRealClosedFieldExports.
Bind Scope ring_scope with ArchiRealClosedField.sort.
#[deprecated(since="mathcomp 2.1.0", note="Require archimedean.v.")]
Notation archiRcfType := archiRcfType (only parsing).
End ArchiRealClosedFieldExports.

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

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

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 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).
#[export]
HB.instance Definition _ := GRing.isDivClosed.Build R Rpos_pred
  pos_divr_closed.

Fact nneg_divr_closed : divr_closed (@nneg R).
#[export]
HB.instance Definition _ := GRing.isDivClosed.Build R Rnneg_pred
  nneg_divr_closed.

Fact nneg_addr_closed : addr_closed (@nneg R).
#[export]
HB.instance Definition _ := GRing.isAddClosed.Build R Rnneg_pred
  nneg_addr_closed.

Fact real_oppr_closed : oppr_closed (@real R).
#[export]
HB.instance Definition _ := GRing.isOppClosed.Build R Rreal_pred
  real_oppr_closed.

Fact real_addr_closed : addr_closed (@real R).
#[export]
HB.instance Definition _ := GRing.isAddClosed.Build R Rreal_pred
  real_addr_closed.

Fact real_divr_closed : divr_closed (@real R).
#[export]
HB.instance Definition _ := GRing.isDivClosed.Build R Rreal_pred
  real_divr_closed.

End NumDomain.

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

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.

Section ArchiNumDomain.
Variable R : ArchiNumDomain.type.
Implicit Types x y : R.

Lemma truncP x :
  if 0 x then (Def.trunc x)%:R x < (Def.trunc x).+1%:R
  else Def.trunc x == 0%N.

Lemma trunc_itv x : 0 x (Def.trunc x)%:R x < (Def.trunc x).+1%:R.

End ArchiNumDomain.

Module Exports. End Exports.

End Internals.

Module PredInstances.

Export Internals.Exports.

End PredInstances.

Module Import ExtraDef.

Definition archi_bound {R : ArchiNumDomain.type} (x : R) := (Def.trunc `|x|).+1.

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

End ExtraDef.

#[deprecated(since="mathcomp 2.1.0", note="Require archimedean.v.")]
Notation bound := archi_bound (only parsing).
Notation sqrt := sqrtr.

Module Import Theory.

Section NumIntegralDomainTheory.

Variable R : numDomainType.
Implicit Types (V : normedZmodType R) (x y z t : R).

Lemmas from the signature (reexported).

Definition ler_normD V (x y : V) : `|x + y| `|x| + `|y| :=
  ler_normD x y.
Definition addr_gt0 x y : 0 < x 0 < y 0 < x + y := @addr_gt0 R x y.
Definition normr0_eq0 V (x : V) : `|x| = 0 x = 0 :=
  @normr0_eq0 R V x.
Definition ger_leVge x y : 0 x 0 y (x y) || (y x) :=
  @ger_leVge R x y.
Definition normrM : {morph norm : x y / (x : R) × y} := @normrM R.
Definition ler_def x y : (x y) = (`|y - x| == y - x) := ler_def x y.
Definition normrMn V (x : V) n : `|x *+ n| = `|x| *+ n := normrMn x n.
Definition normrN V (x : V) : `|- x| = `|x| := normrN x.

Predicate definitions.

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 nposrE x : (x \is npos) = (x 0).
Lemma realE x : (x \is real) = (0 x) || (x 0).

General properties of <= and <

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 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 Extern 0 (is_true (@Order.le ring_display _ _ _)) ⇒
  (apply: ler01) : core.
Hint Extern 0 (is_true (@Order.lt ring_display _ _ _)) ⇒
  (apply: ltr01) : core.
Hint Extern 0 (is_true (@Order.le ring_display _ _ _)) ⇒
  (apply: ler0n) : core.
Lemma ltr0Sn n : 0 < n.+1%:R :> R.
Lemma ltr0n n : (0 < n%:R :> R) = (0 < n)%N.
Hint Extern 0 (is_true (@Order.lt ring_display _ _ _)) ⇒
  (apply: 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 normr1 : `|1 : R| = 1.
Lemma normr_nat n : `|n%:R : R| = n%:R.

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 *) R) : x / x \is a GRing.unit}.

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

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

Lemma big_real x0 op I (P : pred I) F (s : seq I) :
  {in real &, x y, op x y \is real} x0 \is real
  {in P, i, F i \is real} \big[op/x0]_(i <- s | P i) F i \is real.

Lemma sum_real I (P : pred I) (F : I R) (s : seq I) :
  {in P, i, F i \is real} \sum_(i <- s | P i) F i \is real.

Lemma prod_real I (P : pred I) (F : I R) (s : seq I) :
  {in P, i, F i \is real} \prod_(i <- s | P i) F i \is real.

Section NormedZmoduleTheory.

Variable V : normedZmodType R.
Implicit Types (v w : V).

Lemma normr0 : `|0 : V| = 0.

Lemma normr0P v : reflect (`|v| = 0) (v == 0).

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

Lemma distrC v w : `|v - w| = `|w - v|.

Lemma normr_id v : `| `|v| | = `|v|.

Lemma normr_ge0 v : 0 `|v|.

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

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

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

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

End NormedZmoduleTheory.

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

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

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

Lemma ger0_le_norm :
  {in nneg &, {mono (@normr _ R) : x y / x y}}.

Lemma gtr0_le_norm :
  {in pos &, {mono (@normr _ R) : x y / x y}}.

Lemma ler0_ge_norm :
  {in npos &, {mono (@normr _ R) : x y / x y >-> x y}}.

Lemma ltr0_ge_norm :
  {in neg &, {mono (@normr _ R) : x y / x y >-> x y}}.

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).
(* FIXME: rewrite pattern *)
Lemma subr_lt0 x y : (y - x < 0) = (y < x).
(* FIXME: rewrite pattern *)

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

Comparability in a numDomain

Lemma comparable0r x : (0 >=< x)%R = (x \is Num.real).

Lemma comparabler0 x : (x >=< 0)%R = (x \is Num.real).

Lemma subr_comparable0 x y : (x - y >=< 0)%R = (x >=< y)%R.

Lemma comparablerE x y : (x >=< y)%R = (x - y \is Num.real).

Lemma comparabler_trans : transitive (comparable : rel R).

Ordered ring properties.

Definition lter01 := (ler01, ltr01).

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

End NumIntegralDomainTheory.

Arguments ler01 {R}.
Arguments ltr01 {R}.
Arguments normr_idP {R x}.
Arguments normr0P {R V v}.
#[global] Hint Extern 0 (is_true (@Order.le ring_display _ _ _)) ⇒
  (apply: ler01) : core.
#[global] Hint Extern 0 (is_true (@Order.lt ring_display _ _ _)) ⇒
  (apply: ltr01) : core.
#[global] Hint Extern 0 (is_true (@Order.le ring_display _ _ _)) ⇒
  (apply: ler0n) : core.
#[global] Hint Extern 0 (is_true (@Order.lt ring_display _ _ _)) ⇒
  (apply: ltr0Sn) : core.
#[global] Hint Extern 0 (is_true (0 norm _)) ⇒ apply: normr_ge0 : core.

Lemma normr_nneg (R : numDomainType) (x : R) : `|x| \is Num.nneg.
#[global] Hint Resolve normr_nneg : core.

Section NumDomainOperationTheory.

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

Comparison and opposite.

Lemma lerN2 : {mono -%R : x y /~ x y :> R}.
Hint Resolve lerN2 : core.
Lemma ltrN2 : {mono -%R : x y /~ x < y :> R}.
Hint Resolve ltrN2 : core.
Definition lterN2 := (lerN2, ltrN2).

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

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

Definition lterNr := (lerNr, ltrNr).

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

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

Definition lterNl := (lerNl, ltrNl).

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

Lemma gtrN x : 0 < x - x < x.

Definition oppr_lte0 := (oppr_le0, oppr_lt0).
Definition oppr_cp0 := (oppr_gte0, oppr_lte0).
Definition lterNE := (oppr_cp0, lterN2).

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.
Lemma real1 : 1 \is @real R.
Lemma realn n : n%:R \is @real R.
#[local] Hint Resolve real0 real1 : core.

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 real_comparable x y : x \is real y \is real x >=< y.

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

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

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 R R R R
    bool bool Set :=
  | LerNotGt of x y : ler_xor_gt x y x x y y (y - x) (y - x) true false
  | GtrNotLe of y < x : ler_xor_gt x y y y x x (x - y) (x - y) false true.

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

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

Lemma real_leP x y : x \is real y \is real
  ler_xor_gt x y (min y x) (min x y) (max y x) (max x y)
                 `|x - y| `|y - x| (x y) (y < x).

Lemma real_ltP x y : x \is real y \is real
  ltr_xor_ge x y (min y x) (min x y) (max y x) (max x y)
             `|x - y| `|y - x| (y x) (x < y).

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

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

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

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

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

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

Lemma real_ge0P x : x \is real ger0_xor_lt0 x
   (min 0 x) (min x 0) (max 0 x) (max x 0)
  `|x| (x < 0) (0 x).

Lemma real_le0P x : x \is real ler0_xor_gt0 x
  (min 0 x) (min x 0) (max 0 x) (max x 0)
  `|x| (0 < x) (x 0).

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

Lemma max_real : {in real &, x y, max x y \is real}.

Lemma min_real : {in real &, x y, min x y \is real}.

Lemma bigmax_real I x0 (r : seq I) (P : pred I) (f : I R):
  x0 \is real {in P, i : I, f i \is real}
  \big[max/x0]_(i <- r | P i) f i \is real.

Lemma bigmin_real I x0 (r : seq I) (P : pred I) (f : I R):
  x0 \is real {in P, i : I, f i \is real}
  \big[min/x0]_(i <- r | P i) f i \is real.

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

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

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

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

Lemma ltrD2l x : {mono +%R x : y z / y < z}.

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

Definition lerD2 := (lerD2l, lerD2r).
Definition ltrD2 := (ltrD2l, ltrD2r).
Definition lterD2 := (lerD2, ltrD2).

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

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

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

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

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

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

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

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

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

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

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

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

Definition lerBDr := (lerBlDr, lerBrDr).
Definition ltrBDr := (ltrBlDr, ltrBrDr).
Definition lterBDr := (lerBDr, ltrBDr).

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

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

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

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

Definition lerBDl := (lerBlDl, lerBrDl).
Definition ltrBDl := (ltrBlDl, ltrBrDl).
Definition lterBDl := (lerBDl, ltrBDl).

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

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

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

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

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

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

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

Lemma gtrBl x y : (x - y < x) = (0 < y).

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

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

Definition cprD := (lerDl, lerDr, gerDl, gerDl,
                    ltrDl, ltrDr, gtrDl, gtrDl).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma ltr_nDr 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 ler_sum_nat (m n : nat) (F G : nat R) :
  ( i, (m i < n)%N F i G i)
  \sum_(m i < n) F i \sum_(m i < n) 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).

Lemma psumr_neq0 (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) = (has (fun iP i && (0 < F i)) r).

Lemma psumr_neq0P (I : finType) (P : pred I) (F : I R) :
     ( i, P i 0 F i) \sum_(i | P i) F i 0
  ( i, P i && (0 < F i)).

mulr and ler/ltr

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

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

Definition lter_pM2l := (ler_pM2l, ltr_pM2l).

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

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

Definition lter_pM2r := (ler_pM2r, ltr_pM2r).

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

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

Definition lter_nM2l := (ler_nM2l, ltr_nM2l).

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

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

Definition lter_nM2r := (ler_nM2r, ltr_nM2r).

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

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

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

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

Binary forms, for backchaining.

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

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

complement for x *+ n and <= or <

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

Lemma ltr_pMn2r 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_pMn2r 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_wMn2r x y n : x < y (x *+ n < y *+ n) = (0 < n)%N.

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

Lemma ler_wMn2r 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 lerMn2r n x y : (x *+ n y *+ n) = ((n == 0) || (x y)).

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

Lemma eqrMn2r 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 eqNr x : (- x == x) = (x == 0).

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

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

Lemma ler_wnMn2l 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_pMn2l x :
  0 < x {mono (@GRing.natmul R x) : m n / (m n)%N >-> m n}.

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

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

Lemma ltr_nMn2l 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).

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.

and reverse direction

Lemma mulr_ge0_gt0 x y : 0 x 0 y (0 < x × y) = (0 < x) && (0 < 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_pMl x y : 0 < y (x × y y) = (x 1).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma ltr_nMr 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_peMl x y : 0 y 1 x y x × y.

Lemma ler_neMl x y : y 0 1 x x × y y.

Lemma ler_peMr x y : 0 y 1 x y y × x.

Lemma ler_neMr x y : y 0 1 x y × x y.

Lemma ler_piMl x y : 0 y x 1 x × y y.

Lemma ler_niMl x y : y 0 x 1 y x × y.

Lemma ler_piMr x y : 0 y x 1 y × x y.

Lemma ler_niMr 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 /