Library mathcomp.algebra.ssrnum

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

This file defines some classes to manipulate number structures, i.e structures with an order and a norm. 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.).

NumDomain (Integral domain with an order and a norm)

numDomainType == interface for a num integral domain. NumDomainType T m == packs the num mixin into a numDomainType. The carrier T must have an integral domain and a partial order structures. [numDomainType of T for S] == T-clone of the numDomainType structure S. [numDomainType of T] == clone of a canonical numDomainType structure on T.

NormedZmodule (Zmodule with a norm)

normedZmodType R == interface for a normed Zmodule structure indexed by numDomainType R. NormedZmodType R T m == pack the normed Zmodule mixin into a normedZmodType. The carrier T must have an integral domain structure. [normedZmodType R of T for S] == T-clone of the normedZmodType R structure S. [normedZmodType R of T] == clone of a canonical normedZmodType R 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 (Partially ordered Closed Field with conjugation)

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

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

realDomainType == interface for a real integral domain. [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 archimedean axiom r into an archiFieldType. The carrier T must have a real field type structure. [archiFieldType of T for S] == T-clone of the archiFieldType structure S. [archiFieldType of T] == clone of a canonical archiFieldType structure on T.

RealClosedField (Real Field with the real closed axiom)

rcfType == interface for a real closed field. RcfType T r == packs the real closed axiom r into a rcfType. The carrier T must have a real field type structure. [rcfType of T] == clone of a canonical realClosedFieldType structure on T. [rcfType of T for S] == T-clone of the realClosedFieldType structure S.
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.real <=> x is real (:= x >= 0 or x < 0). Num.bound x == in archimedean fields, and upper bound for x, i.e., and n such that `|x| < n%:R. Num.sqrt x == in a real-closed field, a positive square root of x if x >= 0, or 0 otherwise. For numeric algebraically closed fields we provide the generic definitions 'i == the imaginary number (:= sqrtC (-1)). 'Re z == the real component of z. 'Im z == the imaginary component of z. z^* == the complex conjugate of z (:= conjC z). sqrtC z == a nonnegative square root of z, i.e., 0 <= sqrt x if 0 <= x. n.-root z == more generally, for n > 0, an nth root of z, chosen with a minimal non-negative argument for n > 1 (i.e., with a maximal real part subject to a nonnegative imaginary part). Note that n.-root (-1) is a primitive 2nth root of unity, an thus not equal to -1 for n odd > 1 (this will be shown in file cyclotomic.v).
  • 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.

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.

Record normed_mixin_of (R T : zmodType)
       (Rorder : Order.POrder.mixin_of (Equality.class R))
       (le_op := Order.POrder.le Rorder)
  := NormedMixin {
  norm_op : T → R;
  _ : ∀ x y, le_op (norm_op (x + y)) (norm_op x + norm_op y);
  _ : ∀ x, norm_op x = 0 → x = 0;
  _ : ∀ x n, norm_op (x *+ n) = norm_op x *+ n;
  _ : ∀ x, norm_op (- x) = norm_op x;
}.

Record mixin_of (R : ringType)
       (Rorder : Order.POrder.mixin_of (Equality.class R))
       (le_op := Order.POrder.le Rorder) (lt_op := Order.POrder.lt Rorder)
       (normed : @normed_mixin_of R R Rorder) (norm_op := norm_op normed)
  := Mixin {
  _ : ∀ x y, lt_op 0 x → lt_op 0 y → lt_op 0 (x + y);
  _ : ∀ 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);
}.


Module NumDomain.

Section ClassDef.
Record class_of T := Class {
  base : GRing.IntegralDomain.class_of T;
  order_mixin : Order.POrder.mixin_of (Equality.class (ring_for T base));
  normed_mixin : normed_mixin_of (ring_for T base) order_mixin;
  mixin : mixin_of normed_mixin;
}.


Structure type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.
Definition pack (b0 : GRing.IntegralDomain.class_of _) om0
           (nm0 : @normed_mixin_of (ring_for T b0) (ring_for T b0) om0)
           (m0 : @mixin_of (ring_for T b0) om0 nm0) :=
  fun bT (b : GRing.IntegralDomain.class_of T)
      & phant_id (@GRing.IntegralDomain.class bT) b ⇒
  fun om & phant_id om0 om ⇒
  fun nm & phant_id nm0 nm ⇒
  fun m & phant_id m0 m ⇒
  @Pack T (@Class T b om nm m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition ringType := @GRing.Ring.Pack cT class.
Definition comRingType := @GRing.ComRing.Pack cT class.
Definition unitRingType := @GRing.UnitRing.Pack cT class.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class.
Definition idomainType := @GRing.IntegralDomain.Pack cT class.
Definition porderType := @Order.POrder.Pack ring_display cT class.
Definition porder_zmodType := @GRing.Zmodule.Pack porderType class.
Definition porder_ringType := @GRing.Ring.Pack porderType class.
Definition porder_comRingType := @GRing.ComRing.Pack porderType class.
Definition porder_unitRingType := @GRing.UnitRing.Pack porderType class.
Definition porder_comUnitRingType := @GRing.ComUnitRing.Pack porderType class.
Definition porder_idomainType := @GRing.IntegralDomain.Pack porderType class.

End ClassDef.

Module Exports.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Coercion order_base : class_of >-> Order.POrder.class_of.
Coercion normed_mixin : class_of >-> normed_mixin_of.
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 porderType : type >-> Order.POrder.type.
Canonical porderType.
Canonical porder_zmodType.
Canonical porder_ringType.
Canonical porder_comRingType.
Canonical porder_unitRingType.
Canonical porder_comUnitRingType.
Canonical porder_idomainType.
Notation numDomainType := type.
Notation NumDomainType T m := (@pack T _ _ _ m _ _ id _ id _ 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 NormedZmodule.

Section ClassDef.

Variable R : numDomainType.

Record class_of (T : Type) := Class {
  base : GRing.Zmodule.class_of T;
  mixin : @normed_mixin_of R (@GRing.Zmodule.Pack T base) (NumDomain.class R);
}.


Structure type (phR : phant R) :=
  Pack { sort; _ : class_of sort }.

Variables (phR : phant R) (T : Type) (cT : type phR).

Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack phR T c.
Definition pack b0 (m0 : @normed_mixin_of R (@GRing.Zmodule.Pack T b0)
                                          (NumDomain.class R)) :=
  Pack phR (@Class T b0 m0).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> GRing.Zmodule.class_of.
Coercion mixin : class_of >-> normed_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.
Notation normedZmodType R := (type (Phant R)).
Notation NormedZmodType R T m := (@pack _ (Phant R) T _ m).
Notation NormedZmodMixin := Mixin.
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 Exports.

End NormedZmodule.
Import NormedZmodule.Exports.

Module NumDomain_joins.
Import NumDomain.
Section NumDomain_joins.

Variables (T : Type) (cT : type).

Notation class := (class cT).
Definition normedZmodType : normedZmodType cT :=
  @NormedZmodule.Pack
     cT (Phant cT) cT (NormedZmodule.Class (NumDomain.normed_mixin class)).
Definition normedZmod_ringType := @GRing.Ring.Pack normedZmodType class.
Definition normedZmod_comRingType := @GRing.ComRing.Pack normedZmodType class.
Definition normedZmod_unitRingType := @GRing.UnitRing.Pack normedZmodType class.
Definition normedZmod_comUnitRingType :=
  @GRing.ComUnitRing.Pack normedZmodType class.
Definition normedZmod_idomainType :=
  @GRing.IntegralDomain.Pack normedZmodType class.
Definition normedZmod_porderType :=
  @Order.POrder.Pack ring_display normedZmodType class.

End NumDomain_joins.

Module Exports.
Coercion normedZmodType : type >-> NormedZmodule.type.
Canonical normedZmodType.
Canonical normedZmod_ringType.
Canonical normedZmod_comRingType.
Canonical normedZmod_unitRingType.
Canonical normedZmod_comUnitRingType.
Canonical normedZmod_idomainType.
Canonical normedZmod_porderType.
End Exports.
End NumDomain_joins.
Export NumDomain_joins.Exports.

Module Import Def.

Definition normr (R : numDomainType) (T : normedZmodType R) : T → R :=
  nosimpl (norm_op (NormedZmodule.class T)).
Arguments normr {R T} x.

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 Def.
Context {R : numDomainType}.
Implicit Types (x : R).

Definition sgr x : R := if x == 0 then 0 else if x < 0 then -1 else 1.
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 (only parsing).
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 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.
End Keys. End Keys.

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

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.

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

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.
Module NumField.

Section ClassDef.

Record class_of R := Class {
  base : NumDomain.class_of R;
  mixin : GRing.Field.mixin_of (num_for R base);
}.

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

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition ringType := @GRing.Ring.Pack cT class.
Definition comRingType := @GRing.ComRing.Pack cT class.
Definition unitRingType := @GRing.UnitRing.Pack cT class.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class.
Definition idomainType := @GRing.IntegralDomain.Pack cT class.
Definition porderType := @Order.POrder.Pack ring_display cT class.
Definition numDomainType := @NumDomain.Pack cT class.
Definition fieldType := @GRing.Field.Pack cT class.
Definition normedZmodType := NormedZmodType numDomainType cT class.
Definition porder_fieldType := @GRing.Field.Pack porderType class.
Definition normedZmod_fieldType := @GRing.Field.Pack normedZmodType class.
Definition numDomain_fieldType := @GRing.Field.Pack numDomainType class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> NumDomain.class_of.
Coercion base2 : class_of >-> GRing.Field.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
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 porderType : type >-> Order.POrder.type.
Canonical porderType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion normedZmodType : type >-> NormedZmodule.type.
Canonical normedZmodType.
Canonical porder_fieldType.
Canonical normedZmod_fieldType.
Canonical numDomain_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 imaginary_mixin_of (R : numDomainType) := ImaginaryMixin {
  imaginary : R;
  conj_op : {rmorphism R → R};
  _ : imaginary ^+ 2 = - 1;
  _ : ∀ x, x × conj_op x = `|x| ^+ 2;
}.

Record class_of R := Class {
  base : NumField.class_of R;
  decField_mixin : GRing.DecidableField.mixin_of (num_for R base);
  closedField_axiom : GRing.ClosedField.axiom (num_for R base);
  conj_mixin : imaginary_mixin_of (num_for R base);
}.

Structure type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone := fun b & phant_id class (b : class_of T) ⇒ Pack b.
Definition pack :=
  fun bT b & phant_id (NumField.class bT) (b : NumField.class_of T) ⇒
  fun mT dec closed
      & phant_id (GRing.ClosedField.class mT)
                 (@GRing.ClosedField.Class
                    _ (@GRing.DecidableField.Class _ b dec) closed) ⇒
  fun mc ⇒ Pack (@Class T b dec closed mc).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition ringType := @GRing.Ring.Pack cT class.
Definition comRingType := @GRing.ComRing.Pack cT class.
Definition unitRingType := @GRing.UnitRing.Pack cT class.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class.
Definition idomainType := @GRing.IntegralDomain.Pack cT class.
Definition porderType := @Order.POrder.Pack ring_display cT class.
Definition numDomainType := @NumDomain.Pack cT class.
Definition fieldType := @GRing.Field.Pack cT class.
Definition numFieldType := @NumField.Pack cT class.
Definition decFieldType := @GRing.DecidableField.Pack cT class.
Definition closedFieldType := @GRing.ClosedField.Pack cT class.
Definition normedZmodType := NormedZmodType numDomainType cT class.
Definition porder_decFieldType := @GRing.DecidableField.Pack porderType class.
Definition normedZmod_decFieldType :=
  @GRing.DecidableField.Pack normedZmodType class.
Definition numDomain_decFieldType :=
  @GRing.DecidableField.Pack numDomainType class.
Definition numField_decFieldType :=
  @GRing.DecidableField.Pack numFieldType class.
Definition porder_closedFieldType := @GRing.ClosedField.Pack porderType class.
Definition normedZmod_closedFieldType :=
  @GRing.ClosedField.Pack normedZmodType class.
Definition numDomain_closedFieldType :=
  @GRing.ClosedField.Pack numDomainType class.
Definition numField_closedFieldType :=
  @GRing.ClosedField.Pack numFieldType class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> NumField.class_of.
Coercion base2 : class_of >-> GRing.ClosedField.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
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 porderType : type >-> Order.POrder.type.
Canonical porderType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion decFieldType : type >-> GRing.DecidableField.type.
Canonical decFieldType.
Coercion numFieldType : type >-> NumField.type.
Canonical numFieldType.
Coercion closedFieldType : type >-> GRing.ClosedField.type.
Canonical closedFieldType.
Coercion normedZmodType : type >-> NormedZmodule.type.
Canonical normedZmodType.
Canonical porder_decFieldType.
Canonical normedZmod_decFieldType.
Canonical numDomain_decFieldType.
Canonical numField_decFieldType.
Canonical porder_closedFieldType.
Canonical normedZmod_closedFieldType.
Canonical numDomain_closedFieldType.
Canonical numField_closedFieldType.
Notation numClosedFieldType := type.
Notation NumClosedFieldType T m := (@pack T _ _ id _ _ _ id m).
Notation "[ 'numClosedFieldType' 'of' T 'for' cT ]" := (@clone T cT _ id)
  (at level 0, format "[ 'numClosedFieldType' 'of' T 'for' cT ]") :
                                                         form_scope.
Notation "[ 'numClosedFieldType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'numClosedFieldType' 'of' T ]") : form_scope.
End Exports.

End ClosedField.
Import ClosedField.Exports.

Module RealDomain.

Section ClassDef.

Record class_of R := Class {
  base : NumDomain.class_of R;
  nmixin : Order.Lattice.mixin_of base;
  lmixin : Order.DistrLattice.mixin_of (Order.Lattice.Class nmixin);
  tmixin : Order.Total.mixin_of base;
}.

Structure type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition pack :=
  fun bT b & phant_id (NumDomain.class bT) (b : NumDomain.class_of T) ⇒
  fun mT n l m &
      phant_id (@Order.Total.class ring_display mT)
               (@Order.Total.Class T (@Order.DistrLattice.Class
                                        T (@Order.Lattice.Class T b n) l) m) ⇒
  Pack (@Class T b n l m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition ringType := @GRing.Ring.Pack cT class.
Definition comRingType := @GRing.ComRing.Pack cT class.
Definition unitRingType := @GRing.UnitRing.Pack cT class.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class.
Definition idomainType := @GRing.IntegralDomain.Pack cT class.
Definition porderType := @Order.POrder.Pack ring_display cT class.
Definition latticeType := @Order.Lattice.Pack ring_display cT class.
Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT class.
Definition orderType := @Order.Total.Pack ring_display cT class.
Definition numDomainType := @NumDomain.Pack cT class.
Definition normedZmodType := NormedZmodType numDomainType cT class.
Definition zmod_latticeType := @Order.Lattice.Pack ring_display zmodType class.
Definition ring_latticeType := @Order.Lattice.Pack ring_display ringType class.
Definition comRing_latticeType :=
  @Order.Lattice.Pack ring_display comRingType class.
Definition unitRing_latticeType :=
  @Order.Lattice.Pack ring_display unitRingType class.
Definition comUnitRing_latticeType :=
  @Order.Lattice.Pack ring_display comUnitRingType class.
Definition idomain_latticeType :=
  @Order.Lattice.Pack ring_display idomainType class.
Definition normedZmod_latticeType :=
  @Order.Lattice.Pack ring_display normedZmodType class.
Definition numDomain_latticeType :=
  @Order.Lattice.Pack ring_display numDomainType class.
Definition zmod_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display zmodType class.
Definition ring_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display ringType class.
Definition comRing_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display comRingType class.
Definition unitRing_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display unitRingType class.
Definition comUnitRing_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display comUnitRingType class.
Definition idomain_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display idomainType class.
Definition normedZmod_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display normedZmodType class.
Definition numDomain_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display numDomainType class.
Definition zmod_orderType := @Order.Total.Pack ring_display zmodType class.
Definition ring_orderType := @Order.Total.Pack ring_display ringType class.
Definition comRing_orderType :=
  @Order.Total.Pack ring_display comRingType class.
Definition unitRing_orderType :=
  @Order.Total.Pack ring_display unitRingType class.
Definition comUnitRing_orderType :=
  @Order.Total.Pack ring_display comUnitRingType class.
Definition idomain_orderType :=
  @Order.Total.Pack ring_display idomainType class.
Definition normedZmod_orderType :=
  @Order.Total.Pack ring_display normedZmodType class.
Definition numDomain_orderType :=
  @Order.Total.Pack ring_display numDomainType class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> NumDomain.class_of.
Coercion base2 : class_of >-> Order.Total.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
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 porderType : type >-> Order.POrder.type.
Canonical porderType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Coercion latticeType : type >-> Order.Lattice.type.
Canonical latticeType.
Coercion distrLatticeType : type >-> Order.DistrLattice.type.
Canonical distrLatticeType.
Coercion orderType : type >-> Order.Total.type.
Canonical orderType.
Coercion normedZmodType : type >-> NormedZmodule.type.
Canonical normedZmodType.
Canonical zmod_latticeType.
Canonical ring_latticeType.
Canonical comRing_latticeType.
Canonical unitRing_latticeType.
Canonical comUnitRing_latticeType.
Canonical idomain_latticeType.
Canonical normedZmod_latticeType.
Canonical numDomain_latticeType.
Canonical zmod_distrLatticeType.
Canonical ring_distrLatticeType.
Canonical comRing_distrLatticeType.
Canonical unitRing_distrLatticeType.
Canonical comUnitRing_distrLatticeType.
Canonical idomain_distrLatticeType.
Canonical normedZmod_distrLatticeType.
Canonical numDomain_distrLatticeType.
Canonical zmod_orderType.
Canonical ring_orderType.
Canonical comRing_orderType.
Canonical unitRing_orderType.
Canonical comUnitRing_orderType.
Canonical idomain_orderType.
Canonical normedZmod_orderType.
Canonical numDomain_orderType.
Notation realDomainType := type.
Notation "[ 'realDomainType' 'of' T ]" := (@pack T _ _ id _ _ _ _ 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;
  nmixin : Order.Lattice.mixin_of base;
  lmixin : Order.DistrLattice.mixin_of (Order.Lattice.Class nmixin);
  tmixin : Order.Total.mixin_of base;
}.

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

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition ringType := @GRing.Ring.Pack cT class.
Definition comRingType := @GRing.ComRing.Pack cT class.
Definition unitRingType := @GRing.UnitRing.Pack cT class.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class.
Definition idomainType := @GRing.IntegralDomain.Pack cT class.
Definition porderType := @Order.POrder.Pack ring_display cT class.
Definition numDomainType := @NumDomain.Pack cT class.
Definition latticeType := @Order.Lattice.Pack ring_display cT class.
Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT class.
Definition orderType := @Order.Total.Pack ring_display cT class.
Definition realDomainType := @RealDomain.Pack cT class.
Definition fieldType := @GRing.Field.Pack cT class.
Definition numFieldType := @NumField.Pack cT class.
Definition normedZmodType := NormedZmodType numDomainType cT class.
Definition field_latticeType :=
  @Order.Lattice.Pack ring_display fieldType class.
Definition field_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display fieldType class.
Definition field_orderType := @Order.Total.Pack ring_display fieldType class.
Definition field_realDomainType := @RealDomain.Pack fieldType class.
Definition numField_latticeType :=
  @Order.Lattice.Pack ring_display numFieldType class.
Definition numField_distrLatticeType :=
  @Order.DistrLattice.Pack ring_display numFieldType class.
Definition numField_orderType :=
  @Order.Total.Pack ring_display numFieldType class.
Definition numField_realDomainType := @RealDomain.Pack numFieldType class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> NumField.class_of.
Coercion base2 : class_of >-> RealDomain.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
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 porderType : type >-> Order.POrder.type.
Canonical porderType.
Coercion numDomainType : type >-> NumDomain.type.
Canonical numDomainType.
Coercion latticeType : type >-> Order.Lattice.type.
Canonical latticeType.
Coercion distrLatticeType : type >-> Order.DistrLattice.type.
Canonical distrLatticeType.
Coercion orderType : type >-> Order.Total.type.
Canonical orderType.
Coercion realDomainType : type >-> RealDomain.type.
Canonical realDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion numFieldType : type >-> NumField.type.
Canonical numFieldType.
Coercion normedZmodType : type >-> NormedZmodule.type.
Canonical normedZmodType.
Canonical field_latticeType.
Canonical field_distrLatticeType.
Canonical field_orderType.
Canonical field_realDomainType.
Canonical numField_latticeType.
Canonical numField_distrLatticeType.
Canonical numField_orderType.
Canonical numField_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;
  mixin : archimedean_axiom (num_for R base)
}.

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

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition ringType := @GRing.Ring.Pack cT class.
Definition comRingType := @GRing.ComRing.Pack cT class.
Definition unitRingType := @GRing.UnitRing.Pack cT class.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class.
Definition idomainType := @GRing.IntegralDomain.Pack cT class.
Definition porderType := @Order.POrder.Pack ring_display cT class.
Definition latticeType := @Order.Lattice.Pack ring_display cT class.
Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT class.
Definition orderType := @Order.Total.Pack ring_display cT class.
Definition numDomainType := @NumDomain.Pack cT class.
Definition realDomainType := @RealDomain.Pack cT class.
Definition fieldType := @GRing.Field.Pack cT class.
Definition numFieldType := @NumField.Pack cT class.
Definition realFieldType := @RealField.Pack cT class.
Definition normedZmodType := NormedZmodType numDomainType cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> RealField.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
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 porderType : type >-> Order.POrder.type.
Canonical porderType.
Coercion latticeType : type >-> Order.Lattice.type.
Canonical latticeType.
Coercion distrLatticeType : type >-> Order.DistrLattice.type.
Canonical distrLatticeType.
Coercion orderType : type >-> Order.Total.type.
Canonical orderType.
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.
Coercion normedZmodType : type >-> NormedZmodule.type.
Canonical normedZmodType.
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;
  mixin : real_closed_axiom (num_for R base)
}.

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

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @GRing.Zmodule.Pack cT class.
Definition ringType := @GRing.Ring.Pack cT class.
Definition comRingType := @GRing.ComRing.Pack cT class.
Definition unitRingType := @GRing.UnitRing.Pack cT class.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT class.
Definition idomainType := @GRing.IntegralDomain.Pack cT class.
Definition porderType := @Order.POrder.Pack ring_display cT class.
Definition latticeType := @Order.Lattice.Pack ring_display cT class.
Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT class.
Definition orderType := @Order.Total.Pack ring_display cT class.
Definition numDomainType := @NumDomain.Pack cT class.
Definition realDomainType := @RealDomain.Pack cT class.
Definition fieldType := @GRing.Field.Pack cT class.
Definition numFieldType := @NumField.Pack cT class.
Definition realFieldType := @RealField.Pack cT class.
Definition normedZmodType := NormedZmodType numDomainType cT class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> RealField.class_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
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 porderType : type >-> Order.POrder.type.
Canonical porderType.
Coercion latticeType : type >-> Order.Lattice.type.
Canonical latticeType.
Coercion distrLatticeType : type >-> Order.DistrLattice.type.
Canonical distrLatticeType.
Coercion orderType : type >-> Order.Total.type.
Canonical orderType.
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.
Coercion normedZmodType : type >-> NormedZmodule.type.
Canonical normedZmodType.
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 NormedZmodule.
Variables (R : numDomainType) (V : normedZmodType R).
Implicit Types (l : R) (x y : V).

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

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

Lemma normrMn x n : `|x *+ n| = `|x| *+ n.

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

End NormedZmodule.

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

Lemmas from the signature

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 : R) × y}.

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

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

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

Fact archi_bound_subproof (R : archiFieldType) : archimedean_axiom R.

Section RealClosed.
Variable R : rcfType.

Lemma poly_ivt : real_closed_axiom R.

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

End RealClosed.

End Internals.

Module PredInstances.

Canonical pos_mulrPred.
Canonical pos_divrPred.

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

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

End PredInstances.

Module Import ExtraDef.

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

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

End ExtraDef.

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

Module Import Theory.

Section NumIntegralDomainTheory.

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

Lemmas from the signature (reexported from internals).

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

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

Lemma char_num : [char R] =i pred0.

Properties of the norm.

Lemma ger0_def x : (0 ≤ x) = (`|x| == x).
Lemma normr_idP {x} : reflect (`|x| = x) (0 ≤ x).
Lemma ger0_norm x : 0 ≤ x → `|x| = x.
Lemma 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).

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

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 Resolve ler01 ltr01 ltr0Sn ler0n : 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.
Hint Resolve real0 : core.

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

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

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

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

Lemma 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 gtrDl x y : (x + y < x) = (y < 0).

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 i ⇒ P 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%N) || (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%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.

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 / 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_iXnr x n : (0 < n)%N → 0 ≤ x → x ≤ 1 → x ^+ n ≤ x.

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

Definition lter_iXnr := (ler_iXnr, ltr_iXnr).

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

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

Definition lter_eXnr := (ler_eXnr, ltr_eXnr).
Definition lter_Xnr := (lter_iXnr, lter_eXnr).

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

Lemma ler_weXn2l 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_iXn2l x :
  0 < x → x < 1 → {mono GRing.exp x : m n / (n ≤ m)%N >-> m ≤ n}.

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

Definition lter_iXn2l := (ler_iXn2l, ltr_iXn2l).

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

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

Definition lter_eXn2l := (ler_eXn2l, ltr_eXn2l).

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

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

Definition lterXn2r := (lerXn2r, ltrXn2r).

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

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

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

Definition lter_pXn2r := (ler_pXn2r, ltr_pXn2r).

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 eqrXn2 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_pV2 :
  {in [pred x in GRing.unit | 0 < x] &, {mono (@GRing.inv R) : x y /~ x ≤ y}}.

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

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

Lemma ltr_nV2 :
  {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).

max and min

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 real_oppr_max : {in real &, {morph -%R : x y / max x y >-> min x y : R}}.

Lemma real_oppr_min : {in real &, {morph -%R : x y / min x y >-> max x y : R}}.

Lemma real_addr_minl : {in real & real & real, @left_distributive R R +%R min}.

Lemma real_addr_minr : {in real & real & real, @right_distributive R R +%R min}.

Lemma real_addr_maxl : {in real & real & real, @left_distributive R R +%R max}.

Lemma real_addr_maxr : {in real & real & real, @right_distributive R R +%R max}.

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

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

Lemma real_maxr_nMr x y z : x ≤ 0 → y \is real → z \is real →
  x × max y z = min (x × y) (x × z).

Lemma real_minr_nMr x y z : x ≤ 0 → y \is real → z \is real →
  x × min y z = max (x × y) (x × z).

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

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

Lemma real_minr_nMl x y z : x ≤ 0 → y \is real → z \is real →
  min y z × x = max (y × x) (z × x).

Lemma real_maxr_nMl x y z : x ≤ 0 → y \is real → z \is real →
  max y z × x = min (y × x) (z × x).

Lemma real_maxrN x : x \is real → max x (- x) = `|x|.

Lemma real_maxNr x : x \is real → max (- x) x = `|x|.

Lemma real_minrN x : x \is real → min x (- x) = - `|x|.

Lemma real_minNr x : x \is real → min (- x) x = - `|x|.

Section RealDomainArgExtremum.

Context {I : finType} (i0 : I).
Context (P : pred I) (F : I → R) (Pi0 : P i0).
Hypothesis F_real : {in P, ∀ i, F i \is real}.

Lemma real_arg_minP : extremum_spec <=%R P F [arg min_(i < i0 | P i) F i].

Lemma real_arg_maxP : extremum_spec >=%R P F [arg max_(i > i0 | P i) F i].

End RealDomainArgExtremum.

norm

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

norm + add

Section NormedZmoduleTheory.

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

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

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

Lemma ler_normB v w : `|v - w| ≤ `|v| + `|w|.

Lemma ler_distD u v w : `|v - w| ≤ `|v - u| + `|u - w|.

Lemma lerB_normD v w : `|v| - `|w| ≤ `|v + w|.

Lemma lerB_dist v w : `|v| - `|w| ≤ `|v - w|.

Lemma ler_dist_dist v w : `| `|v| - `|w| | ≤ `|v - w|.

Lemma ler_dist_normD v w : `| `|v| - `|w| | ≤ `|v + w|.

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

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

Definition lter_nnormr := (ler_nnorml, ltr_nnorml).

End NormedZmoduleTheory.

Hint Extern 0 (is_true (norm _ \is real)) ⇒ apply: normr_real : core.

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).
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).
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 real_ltr_normlW x y : x \is real → `|x| < y → x < y.

Lemma real_ltrNnormlW x y : x \is real → `|x| < y → - y < x.

Lemma real_ler_normlW x y : x \is real → `|x| ≤ y → x ≤ y.

Lemma real_lerNnormlW x y : x \is real → `|x| ≤ y → - y ≤ x.

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

Lemma real_ltr_distlDr x y e : x - y \is real → `|x - y| < e → x < y + e.

Lemma real_ler_distlDr x y e : x - y \is real → `|x - y| ≤ e → x ≤ y + e.

Lemma real_ltr_distlCDr x y e : x - y \is real → `|x - y| < e → y < x + e.

Lemma real_ler_distlCDr x y e : x - y \is real → `|x - y| ≤ e → y ≤ x + e.

Lemma real_ltr_distlBl x y e : x - y \is real → `|x - y| < e → x - e < y.

Lemma real_ler_distlBl x y e : x - y \is real → `|x - y| ≤ e → x - e ≤ y.

Lemma real_ltr_distlCBl x y e : x - y \is real → `|x - y| < e → y - e < x.

Lemma real_ler_distlCBl x y e : x - y \is real → `|x - y| ≤ e → y - e ≤ x.

(* 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 : R| = 1.

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.

leif

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

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

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

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

Lemma leif_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 leif_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_leif_norm x : x \is real → x ≤ `|x| ?= iff (0 ≤ x).

Lemma leif_pM 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 leif_nM 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 leif_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].

lteif

Lemma subr_lteifr0 C x y : (y - x < 0 ?<= if C) = (y < x ?<= if C).

Lemma subr_lteif0r C x y : (0 < y - x ?<= if C) = (x < y ?<= if C).

Definition subr_lteif0 := (subr_lteifr0, subr_lteif0r).

Lemma lteif01 C : 0 < 1 ?<= if C :> R.

Lemma lteifNl C x y : - x < y ?<= if C = (- y < x ?<= if C).

Lemma lteifNr C x y : x < - y ?<= if C = (y < - x ?<= if C).

Lemma lteif0Nr C x : 0 < - x ?<= if C = (x < 0 ?<= if C).

Lemma lteifNr0 C x : - x < 0 ?<= if C = (0 < x ?<= if C).

Lemma lteifN2 C : {mono -%R : x y /~ x < y ?<= if C :> R}.

Definition lteif_oppE := (lteif0Nr, lteifNr0, lteifN2).

Lemma lteifD2l C x : {mono +%R x : y z / y < z ?<= if C}.

Lemma lteifD2r C x : {mono +%R^~ x : y z / y < z ?<= if C}.

Definition lteifD2 := (lteifD2l, lteifD2r).

Lemma lteifBlDr C x y z : (x - y < z ?<= if C) = (x < z + y ?<= if C).

Lemma lteifBrDr C x y z : (x < y - z ?<= if C) = (x + z < y ?<= if C).

Definition lteifBDr := (lteifBlDr, lteifBrDr).

Lemma lteifBlDl C x y z : (x - y < z ?<= if C) = (x < y + z ?<= if C).

Lemma lteifBrDl C x y z : (x < y - z ?<= if C) = (z + x < y ?<= if C).

Definition lteifBDl := (lteifBlDl, lteifBrDl).

Lemma lteif_pM2l C x : 0 < x → {mono *%R x : y z / y < z ?<= if C}.

Lemma lteif_pM2r C x : 0 < x → {mono *%R^~ x : y z / y < z ?<= if C}.

Lemma lteif_nM2l C x : x < 0 → {mono *%R x : y z /~ y < z ?<= if C}.

Lemma lteif_nM2r C x : x < 0 → {mono *%R^~ x : y z /~ y < z ?<= if C}.

Lemma lteif_nnormr C x y : y < 0 ?<= if ~~ C → (`|x| < y ?<= if C) = false.

Lemma real_lteifNE x y C : x \is Num.real → y \is Num.real →
  x < y ?<= if ~~ C = ~~ (y < x ?<= if C).

Lemma real_lteif_norml C x y :
  x \is Num.real →
  (`|x| < y ?<= if C) = ((- y < x ?<= if C) && (x < y ?<= if C)).

Lemma real_lteif_normr C x y :
  y \is Num.real →
  (x < `|y| ?<= if C) = ((x < y ?<= if C) || (x < - y ?<= if C)).

Lemma real_lteif_distl C x y e :
  x - y \is real →
  (`|x - y| < e ?<= if C) = (y - e < x ?<= if C) && (x < y + e ?<= if C).

Mean inequalities.

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

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

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

#[deprecated(since="mathcomp 1.17.0", note="Use lerN2 instead.")]
Notation ler_opp2 := lerN2.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrN2 instead.")]
Notation ltr_opp2 := ltrN2.
#[deprecated(since="mathcomp 1.17.0", note="Use lterN2 instead.")]
Notation lter_opp2 := lterN2.
#[deprecated(since="mathcomp 1.17.0", note="Use lerNr instead.")]
Notation ler_oppr := lerNr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrNr instead.")]
Notation ltr_oppr := ltrNr.
#[deprecated(since="mathcomp 1.17.0", note="Use lterNr instead.")]
Notation lter_oppr := lterNr.
#[deprecated(since="mathcomp 1.17.0", note="Use lerNl instead.")]
Notation ler_oppl := lerNl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrNl instead.")]
Notation ltr_oppl := ltrNl.
#[deprecated(since="mathcomp 1.17.0", note="Use lterNl instead.")]
Notation lter_oppl := lterNl.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifN2 instead.")]
Notation lteif_opp2 := lteifN2.
#[deprecated(since="mathcomp 1.17.0", note="Use lerD2l instead.")]
Notation ler_add2l := lerD2l.
#[deprecated(since="mathcomp 1.17.0", note="Use lerD2r instead.")]
Notation ler_add2r := lerD2r.
#[deprecated(since="mathcomp 1.17.0", note="Use lerD2 instead.")]
Notation ler_add2 := lerD2.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrD2l instead.")]
Notation ltr_add2l := ltrD2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrD2r instead.")]
Notation ltr_add2r := ltrD2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrD2 instead.")]
Notation ltr_add2 := ltrD2.
#[deprecated(since="mathcomp 1.17.0", note="Use lterD2 instead.")]
Notation lter_add2 := lterD2.
#[deprecated(since="mathcomp 1.17.0", note="Use lerD instead.")]
Notation ler_add := lerD.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_ltD instead.")]
Notation ler_lt_add := ler_ltD.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_leD instead.")]
Notation ltr_le_add := ltr_leD.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrD instead.")]
Notation ltr_add := ltrD.
#[deprecated(since="mathcomp 1.17.0", note="Use lerB instead.")]
Notation ler_sub := lerB.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_ltB instead.")]
Notation ler_lt_sub := ler_ltB.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_leB instead.")]
Notation ltr_le_sub := ltr_leB.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrB instead.")]
Notation ltr_sub := ltrB.
#[deprecated(since="mathcomp 1.17.0", note="Use lerBlDr instead.")]
Notation ler_subl_addr := lerBlDr.
#[deprecated(since="mathcomp 1.17.0", note="Use lerBrDr instead.")]
Notation ler_subr_addr := lerBrDr.
#[deprecated(since="mathcomp 1.17.0", note="Use lerBDr instead.")]
Notation ler_sub_addr := lerBDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrBlDr instead.")]
Notation ltr_subl_addr := ltrBlDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrBrDr instead.")]
Notation ltr_subr_addr := ltrBrDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrBDr instead.")]
Notation ltr_sub_addr := ltrBDr.
#[deprecated(since="mathcomp 1.17.0", note="Use lterBDr instead.")]
Notation lter_sub_addr := lterBDr.
#[deprecated(since="mathcomp 1.17.0", note="Use lerBlDl instead.")]
Notation ler_subl_addl := lerBlDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrBlDl instead.")]
Notation ltr_subl_addl := ltrBlDl.
#[deprecated(since="mathcomp 1.17.0", note="Use lerBrDl instead.")]
Notation ler_subr_addl := lerBrDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrBrDl instead.")]
Notation ltr_subr_addl := ltrBrDl.
#[deprecated(since="mathcomp 1.17.0", note="Use lerBDl instead.")]
Notation ler_sub_addl := lerBDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrBDl instead.")]
Notation ltr_sub_addl := ltrBDl.
#[deprecated(since="mathcomp 1.17.0", note="Use lterBDl instead.")]
Notation lter_sub_addl := lterBDl.
#[deprecated(since="mathcomp 1.17.0", note="Use lerDl instead.")]
Notation ler_addl := lerDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrDl instead.")]
Notation ltr_addl := ltrDl.
#[deprecated(since="mathcomp 1.17.0", note="Use lerDr instead.")]
Notation ler_addr := lerDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrDr instead.")]
Notation ltr_addr := ltrDr.
#[deprecated(since="mathcomp 1.17.0", note="Use gerDl instead.")]
Notation ger_addl := gerDl.
#[deprecated(since="mathcomp 1.17.0", note="Use gtrDl instead.")]
Notation gtr_addl := gtrDl.
#[deprecated(since="mathcomp 1.17.0", note="Use gerDr instead.")]
Notation ger_addr := gerDr.
#[deprecated(since="mathcomp 1.17.0", note="Use gtrDr instead.")]
Notation gtr_addr := gtrDr.
#[deprecated(since="mathcomp 1.17.0", note="Use cprD instead.")]
Notation cpr_add := cprD.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifD2l instead.")]
Notation lteif_add2l := lteifD2l.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifD2r instead.")]
Notation lteif_add2r := lteifD2r.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifD2 instead.")]
Notation lteif_add2 := lteifD2.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifBlDr instead.")]
Notation lteif_subl_addr := lteifBlDr.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifBrDr instead.")]
Notation lteif_subr_addr := lteifBrDr.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifBDr instead.")]
Notation lteif_sub_addr := lteifBDr.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifBlDl instead.")]
Notation lteif_subl_addl := lteifBlDl.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifBrDl instead.")]
Notation lteif_subr_addl := lteifBrDl.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifBDl instead.")]
Notation lteif_sub_addl := lteifBDl.
#[deprecated(since="mathcomp 1.17.0", note="Use leifD instead.")]
Notation leif_add := leifD.
#[deprecated(since="mathcomp 1.17.0", note="Use gtrN instead.")]
Notation gtr_opp := gtrN.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifNl instead.")]
Notation lteif_oppl := lteifNl.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifNr instead.")]
Notation lteif_oppr := lteifNr.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif0Nr instead.")]
Notation lteif_0oppr := lteif0Nr.
#[deprecated(since="mathcomp 1.17.0", note="Use lteifNr0 instead.")]
Notation lteif_oppr0 := lteifNr0.
#[deprecated(since="mathcomp 1.17.0", note="Use lterNE instead.")]
Notation lter_oppE := lterNE.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_distD instead.")]
Notation ler_dist_add := ler_distD.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_dist_normD instead.")]
Notation ler_dist_norm_add := ler_dist_normD.
#[deprecated(since="mathcomp 1.17.0", note="Use lerB_normD instead.")]
Notation ler_sub_norm_add := lerB_normD.
#[deprecated(since="mathcomp 1.17.0", note="Use lerB_dist instead.")]
Notation ler_sub_dist := lerB_dist.
#[deprecated(since="mathcomp 1.17.0", note="Use lerB_real instead.")]
Notation ler_sub_real := lerB_real.
#[deprecated(since="mathcomp 1.17.0", note="Use gerB_real instead.")]
Notation ger_sub_real := gerB_real.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrXn2r instead.")]
Notation ltr_expn2r := ltrXn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use lerXn2r instead.")]
Notation ler_expn2r := lerXn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use lterXn2r instead.")]
Notation lter_expn2r := lterXn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pM instead.")]
Notation ler_pmul := ler_pM.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pM instead.")]
Notation ltr_pmul := ltr_pM.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pV2 instead.")]
Notation ler_pinv := ler_pV2.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nV2 instead.")]
Notation ler_ninv := ler_nV2.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pV2 instead.")]
Notation ltr_pinv := ltr_pV2.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nV2 instead.")]
Notation ltr_ninv := ltr_nV2.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pM2l instead.")]
Notation ler_pmul2l := ler_pM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pM2l instead.")]
Notation ltr_pmul2l := ltr_pM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_pM2l instead.")]
Notation lter_pmul2l := lter_pM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pM2r instead.")]
Notation ler_pmul2r := ler_pM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pM2r instead.")]
Notation ltr_pmul2r := ltr_pM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_pM2r instead.")]
Notation lter_pmul2r := lter_pM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nM2l instead.")]
Notation ler_nmul2l := ler_nM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nM2l instead.")]
Notation ltr_nmul2l := ltr_nM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_nM2l instead.")]
Notation lter_nmul2l := lter_nM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nM2r instead.")]
Notation ler_nmul2r := ler_nM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nM2r instead.")]
Notation ltr_nmul2r := ltr_nM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_nM2r instead.")]
Notation lter_nmul2r := lter_nM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use minr_pMr instead.")]
Notation minr_pmulr := minr_pMr.
#[deprecated(since="mathcomp 1.17.0", note="Use maxr_pMr instead.")]
Notation maxr_pmulr := maxr_pMr.
#[deprecated(since="mathcomp 1.17.0", note="Use minr_pMl instead.")]
Notation minr_pmull := minr_pMl.
#[deprecated(since="mathcomp 1.17.0", note="Use maxr_pMl instead.")]
Notation maxr_pmull := maxr_pMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_wpXn2r instead.")]
Notation ltr_wpexpn2r := ltr_wpXn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pXn2r instead.")]
Notation ler_pexpn2r := ler_pXn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pXn2r instead.")]
Notation ltr_pexpn2r := ltr_pXn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_pXn2r instead.")]
Notation lter_pexpn2r := lter_pXn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ger_pMl instead.")]
Notation ger_pmull := ger_pMl.
#[deprecated(since="mathcomp 1.17.0", note="Use gtr_pMl instead.")]
Notation gtr_pmull := gtr_pMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ger_pMr instead.")]
Notation ger_pmulr := ger_pMr.
#[deprecated(since="mathcomp 1.17.0", note="Use gtr_pMr instead.")]
Notation gtr_pmulr := gtr_pMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pMl instead.")]
Notation ler_pmull := ler_pMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pMl instead.")]
Notation ltr_pmull := ltr_pMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pMr instead.")]
Notation ler_pmulr := ler_pMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pMr instead.")]
Notation ltr_pmulr := ltr_pMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ger_nMl instead.")]
Notation ger_nmull := ger_nMl.
#[deprecated(since="mathcomp 1.17.0", note="Use gtr_nMl instead.")]
Notation gtr_nmull := gtr_nMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ger_nMr instead.")]
Notation ger_nmulr := ger_nMr.
#[deprecated(since="mathcomp 1.17.0", note="Use gtr_nMr instead.")]
Notation gtr_nmulr := gtr_nMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nMl instead.")]
Notation ler_nmull := ler_nMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nMl instead.")]
Notation ltr_nmull := ltr_nMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nMr instead.")]
Notation ler_nmulr := ler_nMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nMr instead.")]
Notation ltr_nmulr := ltr_nMr.
#[deprecated(since="mathcomp 1.17.0", note="Use leif_pM instead.")]
Notation leif_pmul := leif_pM.
#[deprecated(since="mathcomp 1.17.0", note="Use leif_nM instead.")]
Notation leif_nmul := leif_nM.
#[deprecated(since="mathcomp 1.17.0", note="Use eqrXn2 instead.")]
Notation eqr_expn2 := eqrXn2.
#[deprecated(since="mathcomp 1.17.0", note="Use real_maxr_nMr instead.")]
Notation real_maxr_nmulr := real_maxr_nMr.
#[deprecated(since="mathcomp 1.17.0", note="Use real_minr_nMr instead.")]
Notation real_minr_nmulr := real_minr_nMr.
#[deprecated(since="mathcomp 1.17.0", note="Use real_minr_nMl instead.")]
Notation real_minr_nmull := real_minr_nMl.
#[deprecated(since="mathcomp 1.17.0", note="Use real_maxr_nMl instead.")]
Notation real_maxr_nmull := real_maxr_nMl.
#[deprecated(since="mathcomp 1.17.0", note="Use real_ltr_distlDr instead.")]
Notation real_ltr_distl_addr := real_ltr_distlDr.
#[deprecated(since="mathcomp 1.17.0", note="Use real_ler_distlDr instead.")]
Notation real_ler_distl_addr := real_ler_distlDr.
#[deprecated(since="mathcomp 1.17.0", note="Use real_ltr_distlCDr instead.")]
Notation real_ltr_distlC_addr := real_ltr_distlCDr.
#[deprecated(since="mathcomp 1.17.0", note="Use real_ler_distlCDr instead.")]
Notation real_ler_distlC_addr := real_ler_distlCDr.
#[deprecated(since="mathcomp 1.17.0", note="Use real_ltr_distlBl instead.")]
Notation real_ltr_distl_subl := real_ltr_distlBl.
#[deprecated(since="mathcomp 1.17.0", note="Use real_ler_distlBl instead.")]
Notation real_ler_distl_subl := real_ler_distlBl.
#[deprecated(since="mathcomp 1.17.0", note="Use real_ltr_distlCBl instead.")]
Notation real_ltr_distlC_subl := real_ltr_distlCBl.
#[deprecated(since="mathcomp 1.17.0", note="Use real_ler_distlCBl instead.")]
Notation real_ler_distlC_subl := real_ler_distlCBl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_iXn2l instead.")]
Notation ler_iexpn2l := ler_iXn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_iXn2l instead.")]
Notation ltr_iexpn2l := ltr_iXn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_iXn2l instead.")]
Notation lter_iexpn2l := lter_iXn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_eXn2l instead.")]
Notation ler_eexpn2l := ler_eXn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_eXn2l instead.")]
Notation ltr_eexpn2l := ltr_eXn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_eXn2l instead.")]
Notation lter_eexpn2l := lter_eXn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpM2l instead.")]
Notation ler_wpmul2l := ler_wpM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpM2rinstead.")]
Notation ler_wpmul2r := ler_wpM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnM2l instead.")]
Notation ler_wnmul2l := ler_wnM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnM2r instead.")]
Notation ler_wnmul2r := ler_wnM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_peMl instead.")]
Notation ler_pemull := ler_peMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_neMl instead.")]
Notation ler_nemull := ler_neMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_peMr instead.")]
Notation ler_pemulr := ler_peMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_neMr instead.")]
Notation ler_nemulr := ler_neMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_iXnr instead.")]
Notation ler_iexpr:= ler_iXnr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_iXnr instead.")]
Notation ltr_iexpr := ltr_iXnr.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_iXnr instead.")]
Notation lter_iexpr := lter_iXnr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_eXnr instead.")]
Notation ler_eexpr := ler_eXnr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_eXnr instead.")]
Notation ltr_eexpr := ltr_eXnr.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_eXnr instead.")]
Notation lter_eexpr := lter_eXnr.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_Xnr instead.")]
Notation lter_expr := lter_Xnr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wiXn2l instead.")]
Notation ler_wiexpn2l := ler_wiXn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_weXn2l instead.")]
Notation ler_weexpn2l := ler_weXn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_piMl instead.")]
Notation ler_pimull := ler_piMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_niMl instead.")]
Notation ler_nimull := ler_niMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_piMr instead.")]
Notation ler_pimulr := ler_piMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_niMr instead.")]
Notation ler_nimulr := ler_niMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pMn2r instead.")]
Notation ler_pmuln2r := ler_pMn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pMn2r instead.")]
Notation ltr_pmuln2r := ltr_pMn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pMn2l instead.")]
Notation ler_pmuln2l := ler_pMn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpMn2l instead.")]
Notation ler_wpmuln2l := ler_wpMn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use eqr_pMn2r instead.")]
Notation eqr_pmuln2r := eqr_pMn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_wMn2r instead.")]
Notation ltr_wmuln2r := ltr_wMn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_wpMn2r instead.")]
Notation ltr_wpmuln2r := ltr_wpMn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wMn2r instead.")]
Notation ler_wmuln2r := ler_wMn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnMn2l instead.")]
Notation ler_wnmuln2l := ler_wnMn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use lerMn2r instead.")]
Notation ler_muln2r := lerMn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltrMn2r instead.")]
Notation ltr_muln2r := ltrMn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use eqrMn2r instead.")]
Notation eqr_muln2r := eqrMn2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pMn2l instead.")]
Notation ltr_pmuln2l := ltr_pMn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_nMn2l instead.")]
Notation ler_nmuln2l := ler_nMn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nMn2l instead.")]
Notation ltr_nmuln2l := ltr_nMn2l.
#[deprecated(since="mathcomp 1.17.0", note="Use leifBLR instead.")]
Notation leif_subLR := leifBLR.
#[deprecated(since="mathcomp 1.17.0", note="Use leifBRL instead.")]
Notation leif_subRL := leifBRL.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_pM2l instead.")]
Notation lteif_pmul2l := lteif_pM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_pM2l instead.")]
Notation lteif_pmul2r := lteif_pM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_nM2l instead.")]
Notation lteif_nmul2l := lteif_nM2l.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_nM2r instead.")]
Notation lteif_nmul2r := lteif_nM2r.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpDl instead.")]
Notation ler_paddl := ler_wpDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_wpDl instead.")]
Notation ltr_paddl := ltr_wpDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pwDl instead.")]
Notation ltr_spaddl := ltr_pwDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pDl instead.")]
Notation ltr_spsaddl := ltr_pDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnDl instead.")]
Notation ler_naddl := ler_wnDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_wnDl instead.")]
Notation ltr_naddl := ltr_wnDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nwDl instead.")]
Notation ltr_snaddl := ltr_nwDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nDl instead.")]
Notation ltr_snsaddl := ltr_nDl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wpDr instead.")]
Notation ler_paddr := ler_wpDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_wpDr instead.")]
Notation ltr_paddr := ltr_wpDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pwDr instead.")]
Notation ltr_spaddr := ltr_pwDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pDr instead.")]
Notation ltr_spsaddr := ltr_pDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_wnDr instead.")]
Notation ler_naddr := ler_wnDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_wnDr instead.")]
Notation ltr_naddr := ltr_wnDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nwDr instead.")]
Notation ltr_snaddr := ltr_nwDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_nDr instead.")]
Notation ltr_snsaddr := ltr_nDr.

#[global] Hint Resolve lerN2 ltrN2 real0 real1 normr_real : core.
Arguments ler_sqr {R} [x y].
Arguments ltr_sqr {R} [x y].
Arguments signr_inj {R} [x1 x2].
Arguments real_ler_normlP {R x y}.
Arguments real_ltr_normlP {R x y}.

Section NumDomainMonotonyTheoryForReals.
Local Open Scope order_scope.

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

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

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

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

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

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

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

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

Lemma realn_nmono_in : {in D &, {homo f' : x y / y < x >-> (x < y)}} →
  {in [pred x in D | x \is real] &, {mono f' : x y / y ≤ x >-> (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_pV2 : {in pos &, {mono (@GRing.inv F) : x y /~ x ≤ y}}.

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

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

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

Definition ltef_pV2 := (lef_pV2, ltf_pV2).
Definition ltef_nV2 := (lef_nV2, ltf_nV2).

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_pdivlMr z x y : 0 < z → (x ≤ y / z) = (x × z ≤ y).

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

Definition lter_pdivlMr := (ler_pdivlMr, ltr_pdivlMr).

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

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

Definition lter_pdivrMr := (ler_pdivrMr, ltr_pdivrMr).

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

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

Definition lter_pdivlMl := (ler_pdivlMl, ltr_pdivlMl).

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

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

Definition lter_pdivrMl := (ler_pdivrMl, ltr_pdivrMl).

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

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

Definition lter_ndivlMr := (ler_ndivlMr, ltr_ndivlMr).

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

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

Definition lter_ndivrMr := (ler_ndivrMr, ltr_ndivrMr).

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

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

Definition lter_ndivlMl := (ler_ndivlMl, ltr_ndivlMl).

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

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

Definition lter_ndivrMl := (ler_ndivrMl, ltr_ndivrMl).

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

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

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

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

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

Lemma splitr x : x = x / 2%:R + x / 2%:R.

lteif

Lemma lteif_pdivlMr C z x y :
  0 < z → x < y / z ?<= if C = (x × z < y ?<= if C).

Lemma lteif_pdivrMr C z x y :
  0 < z → y / z < x ?<= if C = (y < x × z ?<= if C).

Lemma lteif_pdivlMl C z x y :
  0 < z → x < z^-1 × y ?<= if C = (z × x < y ?<= if C).

Lemma lteif_pdivrMl C z x y :
  0 < z → z^-1 × y < x ?<= if C = (y < z × x ?<= if C).

Lemma lteif_ndivlMr C z x y :
  z < 0 → x < y / z ?<= if C = (y < x × z ?<= if C).

Lemma lteif_ndivrMr C z x y :
  z < 0 → y / z < x ?<= if C = (x × z < y ?<= if C).

Lemma lteif_ndivlMl C z x y :
  z < 0 → x < z^-1 × y ?<= if C = (y < z × x ?<= if C).

Lemma lteif_ndivrMl C z x y :
  z < 0 → z^-1 × y < x ?<= if C = (z × x < y ?<= if C).

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

Lemma ler_addgt0Pr x y : reflect (∀ e, e > 0 → x ≤ y + e) (x ≤ y).

Lemma ler_addgt0Pl x y : reflect (∀ e, e > 0 → x ≤ e + y) (x ≤ y).

Lemma lt_le a b : (∀ x, x < a → x < b) → a ≤ b.

Lemma gt_ge a b : (∀ x, b < x → a < x) → a ≤ b.

The AGM, unscaled but without the nth root.

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

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

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

#[deprecated(since="mathcomp 1.17.0", note="Use lef_pV2 instead.")]
Notation lef_pinv := lef_pV2.
#[deprecated(since="mathcomp 1.17.0", note="Use lef_nV2 instead.")]
Notation lef_ninv := lef_nV2.
#[deprecated(since="mathcomp 1.17.0", note="Use ltf_pV2 instead.")]
Notation ltf_pinv := ltf_pV2.
#[deprecated(since="mathcomp 1.17.0", note="Use ltf_nV2 instead.")]
Notation ltf_ninv := ltf_nV2.
#[deprecated(since="mathcomp 1.17.0", note="Use ltef_pV2 instead.")]
Notation ltef_pinv := ltef_pV2.
#[deprecated(since="mathcomp 1.17.0", note="Use ltef_nV2 instead.")]
Notation ltef_ninv := ltef_nV2.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_pdivlMr instead.")]
Notation lteif_pdivl_mulr := lteif_pdivlMr.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_pdivrMr instead.")]
Notation lteif_pdivr_mulr := lteif_pdivrMr.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_pdivlMl instead.")]
Notation lteif_pdivl_mull := lteif_pdivlMl.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_pdivrMl instead.")]
Notation lteif_pdivr_mull := lteif_pdivrMl.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_ndivlMr instead.")]
Notation lteif_ndivl_mulr := lteif_ndivlMr.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_ndivrMr instead.")]
Notation lteif_ndivr_mulr := lteif_ndivrMr.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_ndivlMl instead.")]
Notation lteif_ndivl_mull := lteif_ndivlMl.
#[deprecated(since="mathcomp 1.17.0", note="Use lteif_ndivrMl instead.")]
Notation lteif_ndivr_mull := lteif_ndivrMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pdivlMr instead.")]
Notation ler_pdivl_mulr := ler_pdivlMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pdivlMr instead.")]
Notation ltr_pdivl_mulr := ltr_pdivlMr.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_pdivlMr instead.")]
Notation lter_pdivl_mulr := lter_pdivlMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pdivrMr instead.")]
Notation ler_pdivr_mulr := ler_pdivrMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pdivrMr instead.")]
Notation ltr_pdivr_mulr := ltr_pdivrMr.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_pdivrMr instead.")]
Notation lter_pdivr_mulr := lter_pdivrMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pdivlMl instead.")]
Notation ler_pdivl_mull := ler_pdivlMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pdivlMl instead.")]
Notation ltr_pdivl_mull := ltr_pdivlMl.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_pdivlMl instead.")]
Notation lter_pdivl_mull := lter_pdivlMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_pdivrMl instead.")]
Notation ler_pdivr_mull := ler_pdivrMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_pdivrMl instead.")]
Notation ltr_pdivr_mull := ltr_pdivrMl.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_pdivrMl instead.")]
Notation lter_pdivr_mull := lter_pdivrMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_ndivlMr instead.")]
Notation ler_ndivl_mulr := ler_ndivlMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_ndivlMr instead.")]
Notation ltr_ndivl_mulr := ltr_ndivlMr.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_ndivlMr instead.")]
Notation lter_ndivl_mulr := lter_ndivlMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_ndivrMr instead.")]
Notation ler_ndivr_mulr := ler_ndivrMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_ndivrMr instead.")]
Notation ltr_ndivr_mulr := ltr_ndivrMr.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_ndivrMr instead.")]
Notation lter_ndivr_mulr := lter_ndivrMr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_ndivlMl instead.")]
Notation ler_ndivl_mull := ler_ndivlMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_ndivlMl instead.")]
Notation ltr_ndivl_mull := ltr_ndivlMl.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_ndivlMl instead.")]
Notation lter_ndivl_mull := lter_ndivlMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_ndivrMl instead.")]
Notation ler_ndivr_mull := ler_ndivrMl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_ndivrMl instead.")]
Notation ltr_ndivr_mull := ltr_ndivrMl.
#[deprecated(since="mathcomp 1.17.0", note="Use lter_ndivrMl instead.")]
Notation lter_ndivr_mull := lter_ndivrMl.

Section RealDomainTheory.

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

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

Lemma lerP x y : 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 ltrP x y : 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 ltrgtP x y :
   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) .

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

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

Lemma ltrgt0P x : 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).

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.

#[global] Hint Resolve num_real : core.

Section RealDomainOperations.

Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
    (Order.arg_min (disp := ring_display) i0 (fun i ⇒ P%B) (fun i ⇒ F)) :
   ring_scope.

Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" :=
  [arg min_(i < i0 | i \in A) F] : ring_scope.

Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true) F] :
  ring_scope.

Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" :=
   (Order.arg_max (disp := ring_display) i0 (fun i ⇒ P%B) (fun i ⇒ F)) :
  ring_scope.

Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" :=
    [arg max_(i > i0 | i \in A) F] : ring_scope.

Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] :
  ring_scope.

sgr section

Variable R : realDomainType.
Implicit Types x y z t : R.
Let numR_real := @num_real R.
Hint Resolve numR_real : core.

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

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

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

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

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

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

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

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

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

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

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

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

norm section

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

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

Lemma ler_normlP x y : reflect ((- x ≤ y) × (x ≤ y)) (`|x| ≤ y).
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).
Arguments ltr_normlP {x y}.

Lemma ltr_normlW x y : `|x| < y → x < y.

Lemma ltrNnormlW x y : `|x| < y → - y < x.

Lemma ler_normlW x y : `|x| ≤ y → x ≤ y.

Lemma lerNnormlW x y : `|x| ≤ y → - y ≤ x.

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 ltr_distlC x y e : (`|x - y| < e) = (x - e < y < x + e).

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

Definition lter_distlC := (ler_distlC, ltr_distlC).

Lemma ltr_distlDr x y e : `|x - y| < e → x < y + e.

Lemma ler_distlDr x y e : `|x - y| ≤ e → x ≤ y + e.

Lemma ltr_distlCDr x y e : `|x - y| < e → y < x + e.

Lemma ler_distlCDr x y e : `|x - y| ≤ e → y ≤ x + e.

Lemma ltr_distlBl x y e : `|x - y| < e → x - e < y.

Lemma ler_distlBl x y e : `|x - y| ≤ e → x - e ≤ y.

Lemma ltr_distlCBl x y e : `|x - y| < e → y - e < x.

Lemma ler_distlCBl x y e : `|x - y| ≤ e → y - e ≤ x.

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

lteif

Lemma lteif_norml C x y :
  (`|x| < y ?<= if C) = (- y < x ?<= if C) && (x < y ?<= if C).

Lemma lteif_normr C x y :
  (x < `|y| ?<= if C) = (x < y ?<= if C) || (x < - y ?<= if C).

Lemma lteif_distl C x y e :
  (`|x - y| < e ?<= if C) = (y - e < x ?<= if C) && (x < y + e ?<= if C).

Special lemmas for squares.

Lemma sqr_ge0 x : 0 ≤ x ^+ 2.

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

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

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

Section MinMax.

Lemma oppr_max : {morph -%R : x y / max x y >-> min x y : R}.

Lemma oppr_min : {morph -%R : x y / min x y >-> max x y : R}.

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 minr_nMr x y z : x ≤ 0 → x × min y z = max (x × y) (x × z).

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

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

Lemma maxr_nMl 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 leif_mean_square : x × y ≤ (x ^+ 2 + y ^+ 2) / 2 ?= iff (x == y).

Lemma leif_AGM2 : x × y ≤ ((x + y) / 2)^+ 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 ^+ i.

End ArchimedeanFieldTheory.

Section RealClosedFieldTheory.

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

Lemma poly_ivt : real_closed_axiom R.

Square Root theory

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

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

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

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

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

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

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

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

Lemma sqrtr0 : sqrt 0 = 0 :> R.

Lemma sqrtr1 : sqrt 1 = 1 :> R.

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

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

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

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

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

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

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

Lemma sqrtrV x : 0 ≤ x → sqrt (x^-1) = (sqrt x)^-1.

End RealClosedFieldTheory.

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

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

Section ClosedFieldTheory.

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

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

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

Lemma mulCii : 'i × 'i = -1 :> C.

Lemma conjCK : involutive (@conjC C).

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

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

Fact rootC_subproof n x : rootC_spec n x.

Definition nthroot n x := let: RootCspec y _ _ := rootC_subproof n x in y.
Notation "n .-root" := (nthroot n) : ring_scope.
Notation sqrtC := 2.-root.

Fact Re_lock : unit.
Fact Im_lock : unit.
Definition Re z := locked_with Re_lock ((z + z^*) / 2%:R).
Definition Im z := locked_with Im_lock ('i × (z^* - z) / 2%:R).
Notation "'Re z" := (Re z) : ring_scope.
Notation "'Im z" := (Im z) : ring_scope.

Lemma ReE z : 'Re z = (z + z^*) / 2%:R.
Lemma ImE z : 'Im z = 'i × (z^* - z) / 2%:R.

Let nz2 : 2 != 0 :> C.

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

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

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

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

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

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

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

Real number subset.

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

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

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

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

Lemma CrealJ : {mono (@conjC C) : x / x \is Num.real}.

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

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

Elementary properties of roots.

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

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

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

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

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

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

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

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

Rectangular coordinates.

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

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

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

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

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

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

Lemma eqCP x y : x = y ↔ ('Re x = 'Re y) ∧ ('Im x = 'Im y).

Lemma eqC x y : (x == y) = ('Re x == 'Re y) && ('Im x == 'Im y).

Lemma Creal_Re x : 'Re x \is real.

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

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

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

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

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

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

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

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

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

Lemma Re_i : 'Re 'i = 0.

Lemma Im_i : 'Im 'i = 1.

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

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

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

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

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

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

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

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

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

Lemma ImM x y : 'Im (x × y) = 'Re x × 'Im y + 'Re y × 'Im x.

Lemma ImMil x : 'Im ('i × x) = 'Re x.

Lemma ReMil x : 'Re ('i × x) = - 'Im x.

Lemma ReMir x : 'Re (x × 'i) = - 'Im x.

Lemma ImMir x : 'Im (x × 'i) = 'Re x.

Lemma ReM x y : 'Re (x × y) = 'Re x × 'Re y - 'Im x × 'Im y.

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

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

Lemma invC_Crect x y : (x + 'i × y)^-1 = (x^* - 'i × y^*) / `|x + 'i × y| ^+ 2.

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

Lemma ImV x : 'Im x^-1 = - 'Im x / `|x| ^+ 2.

Lemma ReV x : 'Re x^-1 = 'Re x / `|x| ^+ 2.

Lemma rectC_mulr x y z : (x + 'i × y) × z = x × z + 'i × (y × z).

Lemma rectC_mull x y z : z × (x + 'i × y) = z × x + 'i × (z × y).

Lemma divC_Crect x1 y1 x2 y2 :
  (x1 + 'i × y1) / (x2 + 'i × y2) =
  (x1 × x2^* + y1 × y2^* + 'i × (x2^* × y1 - x1 × y2^*)) /
    `|x2 + 'i × y2| ^+ 2.

Lemma divC_rect x1 y1 x2 y2 :
     x1 \is real → y1 \is real → x2 \is real → y2 \is real →
  (x1 + 'i × y1) / (x2 + 'i × y2) =
  (x1 × x2 + y1 × y2 + 'i × (x2 × y1 - x1 × y2)) /
    (x2 ^+ 2 + y2 ^+ 2).

Lemma Im_div x y : 'Im (x / y) = ('Re y × 'Im x - 'Re x × 'Im y) / `|y| ^+ 2.

Lemma Re_div x y : 'Re (x / y) = ('Re x × 'Re y + 'Im x × 'Im y) / `|y| ^+ 2.

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

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

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

Nth roots.

Let argCleP y z :
  reflect (0 ≤ 'Im z → 0 ≤ 'Im y ∧ 'Re z ≤ 'Re y) (argCle y z).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Square root.

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

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

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

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

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

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

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

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

Norm sum (in)equalities.

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

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

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

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

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

End ClosedFieldTheory.
#[deprecated(since="mathcomp 1.17.0", note="Use normCDeq instead.")]
Notation normC_add_eq := normCDeq.
#[deprecated(since="mathcomp 1.17.0", note="Use normCBeq instead.")]
Notation normC_sub_eq := normCBeq.

Notation "n .-root" := (@nthroot _ n).
Notation sqrtC := 2.-root.
Notation "'i" := (@imaginaryC _) : ring_scope.
Notation "'Re z" := (Re z) : ring_scope.
Notation "'Im z" := (Im z) : ring_scope.

Arguments conjCK {C} x.
Arguments sqrCK {C} [x] le0x.
Arguments sqrCK_P {C x}.

#[global] Hint Extern 0 (is_true (in_mem ('Re _) _)) ⇒
  solve [apply: Creal_Re] : core.
#[global] Hint Extern 0 (is_true (in_mem ('Im _) _)) ⇒
  solve [apply: Creal_Im] : core.

End Theory.

FACTORIES

Module NumMixin.
Section NumMixin.
Variable (R : idomainType).

Record of_ := Mixin {
  le : rel R;
  lt : rel R;
  norm : R → R;
  normD : ∀ x y, le (norm (x + y)) (norm x + norm y);
  addr_gt0 : ∀ x y, lt 0 x → lt 0 y → lt 0 (x + y);
  norm_eq0 : ∀ x, norm x = 0 → x = 0;
  ger_total : ∀ x y, le 0 x → le 0 y → le x y || le y x;
  normM : {morph norm : x y / x × y};
  le_def : ∀ x y, (le x y) = (norm (y - x) == y - x);
  lt_def : ∀ x y, (lt x y) = (y != x) && (le x y)
}.

Variable (m : of_).


Lemma ltrr x : x < x = false.

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

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

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

Lemma lt_trans : transitive (lt m).

Lemma le01 : 0 ≤ 1.

Lemma lt01 : 0 < 1.

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

Lemma lerr x : x ≤ x.

Lemma le_def' x y : (x ≤ y) = (x == y) || (x < y).

Lemma le_trans : transitive (le m).

Lemma normrMn x n : `|x *+ n| = `|x| *+ n.

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

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

Definition ltPOrderMixin : ltPOrderMixin R :=
  LtPOrderMixin le_def' ltrr lt_trans.

Definition normedZmodMixin :
  @normed_mixin_of R R ltPOrderMixin :=
  @Num.NormedMixin _ _ ltPOrderMixin (norm m)
                   (normD m) (@norm_eq0 m) normrMn normrN.

Definition numDomainMixin :
  @mixin_of R ltPOrderMixin normedZmodMixin :=
  @Num.Mixin _ ltPOrderMixin normedZmodMixin (@addr_gt0 m)
             (@ger_total m) (@normM m) (@le_def m).

End NumMixin.

Module Exports.
Notation numMixin := of_.
Notation NumMixin := Mixin.
Coercion ltPOrderMixin : numMixin >-> Order.LtPOrderMixin.of_.
Coercion normedZmodMixin : numMixin >-> normed_mixin_of.
Coercion numDomainMixin : numMixin >-> mixin_of.
Definition NumDomainOfIdomain (T : idomainType) (m : of_ T) :=
  NumDomainType (POrderType ring_display T m) m.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_normD instead.")]
Notation ler_norm_add := ler_normD.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_normB instead.")]
Notation ler_norm_sub := ler_normB.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_distlDr instead.")]
Notation ltr_distl_addr := ltr_distlDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_distlDr instead.")]
Notation ler_distl_addr := ler_distlDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_distlCDr instead.")]
Notation ltr_distlC_addr := ltr_distlCDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_distlCDr instead.")]
Notation ler_distlC_addr := ler_distlCDr.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_distlBl instead.")]
Notation ltr_distl_subl := ltr_distlBl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_distlBl instead.")]
Notation ler_distl_subl := ler_distlBl.
#[deprecated(since="mathcomp 1.17.0", note="Use ltr_distlCBl instead.")]
Notation ltr_distlC_subl := ltr_distlCBl.
#[deprecated(since="mathcomp 1.17.0", note="Use ler_distlCBl instead.")]
Notation ler_distlC_subl := ler_distlCBl.
#[deprecated(since="mathcomp 1.17.0", note="Use maxr_nMr instead.")]
Notation maxr_nmulr := maxr_nMr.
#[deprecated(since="mathcomp 1.17.0", note="Use minr_nMr instead.")]
Notation minr_nmulr := minr_nMr.
#[deprecated(since="mathcomp 1.17.0", note="Use minr_nMl instead.")]
Notation minr_nmull := minr_nMl.
#[deprecated(since="mathcomp 1.17.0", note="Use maxr_nMl instead.")]
Notation maxr_nmull := maxr_nMl.
End Exports.

End NumMixin.
Import NumMixin.Exports.

Module RealMixin.
Section RealMixin.
Variables (R : numDomainType).

Variable (real : real_axiom R).

Lemma le_total : totalPOrderMixin R.

End RealMixin.

Module Exports.
Coercion le_total : real_axiom >-> totalPOrderMixin.
Definition RealDomainOfNumDomain (T : numDomainType) (m : real_axiom T) :=
  [realDomainType of OrderOfPOrder m].
End Exports.

End RealMixin.
Import RealMixin.Exports.

Module RealLeMixin.
Section RealLeMixin.
Variables (R : idomainType).

Record of_ := Mixin {
  le : rel R;
  lt : rel R;
  norm : R → R;
  le0_add : ∀ x y, le 0 x → le 0 y → le 0 (x + y);
  le0_mul : ∀ x y, le 0 x → le 0 y → le 0 (x × y);
  le0_anti : ∀ x, le 0 x → le x 0 → x = 0;
  sub_ge0 : ∀ x y, le 0 (y - x) = le x y;
  le0_total : ∀ x, le 0 x || le x 0;
  normN : ∀ x, norm (- x) = norm x;
  ge0_norm : ∀ x, le 0 x → norm x = x;
  lt_def : ∀ x y, lt x y = (y != x) && le x y;
}.

Variable (m : of_).


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

Let le00 : 0 ≤ 0.

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 m : x y / x × y}.

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

Fact le_total : total (le m).

Definition numMixin : numMixin R :=
  NumMixin le_normD lt0_add eq0_norm (in2W le_total) normM le_def (lt_def m).

Definition orderMixin :
  totalPOrderMixin (POrderType ring_display R numMixin) :=
  le_total.

End RealLeMixin.

Module Exports.
Notation realLeMixin := of_.
Notation RealLeMixin := Mixin.
Coercion numMixin : realLeMixin >-> NumMixin.of_.
Coercion orderMixin : realLeMixin >-> totalPOrderMixin.
Definition LeRealDomainOfIdomain (R : idomainType) (m : of_ R) :=
  [realDomainType of @OrderOfPOrder _ (NumDomainOfIdomain m) m].
Definition LeRealFieldOfField (R : fieldType) (m : of_ R) :=
  [realFieldType of [numFieldType of LeRealDomainOfIdomain m]].
End Exports.

End RealLeMixin.
Import RealLeMixin.Exports.

Module RealLtMixin.
Section RealLtMixin.
Variables (R : idomainType).

Record of_ := Mixin {
  lt : rel R;
  le : rel R;
  norm : R → R;
  lt0_add : ∀ x y, lt 0 x → lt 0 y → lt 0 (x + y);
  lt0_mul : ∀ x y, lt 0 x → lt 0 y → lt 0 (x × y);
  lt0_ngt0 : ∀ x, lt 0 x → ~~ (lt x 0);
  sub_gt0 : ∀ x y, lt 0 (y - x) = lt x y;
  lt0_total : ∀ x, x != 0 → lt 0 x || lt x 0;
  normN : ∀ x, norm (- x) = norm x;
  ge0_norm : ∀ x, le 0 x → norm x = x;
  le_def : ∀ x y, le x y = (x == y) || lt x y;
}.

Variable (m : of_).


Fact lt0N x : (- x < 0) = (0 < x).
Let leN_total x : 0 ≤ x ∨ 0 ≤ - x.

Let le00 : (0 ≤ 0).

Fact sub_ge0 x y : (0 ≤ 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 normM : {morph norm m : x y / x × y}.

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

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

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

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

Fact le_total : total (le m).

Definition numMixin : numMixin R :=
  NumMixin le_normD (@lt0_add m) eq0_norm (in2W le_total) normM le_def' lt_def.

Definition orderMixin :
  totalPOrderMixin (POrderType ring_display R numMixin) :=
  le_total.

End RealLtMixin.

Module Exports.
Notation realLtMixin := of_.
Notation RealLtMixin := Mixin.
Coercion numMixin : realLtMixin >-> NumMixin.of_.
Coercion orderMixin : realLtMixin >-> totalPOrderMixin.
Definition LtRealDomainOfIdomain (R : idomainType) (m : of_ R) :=
  [realDomainType of @OrderOfPOrder _ (NumDomainOfIdomain m) m].
Definition LtRealFieldOfField (R : fieldType) (m : of_ R) :=
  [realFieldType of [numFieldType of LtRealDomainOfIdomain m]].
End Exports.

End RealLtMixin.
Import RealLtMixin.Exports.

End Num.

Export Num.NumDomain.Exports Num.NormedZmodule.Exports.
Export Num.NumDomain_joins.Exports.
Export 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.
Export Num.NumMixin.Exports Num.RealMixin.Exports.
Export Num.RealLeMixin.Exports Num.RealLtMixin.Exports.

Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin.