- -

Library mathcomp.algebra.ssrnum

- -

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

- -

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

- -

NumDomain (Integral domain with an order and a norm)

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

- -

NumField (Field with an order and a norm)

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

- -

NumClosedField (Closed Field with an order and a norm)

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

- -

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

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

- -

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

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

- -

ArchiField (A Real Field with the archimedean axiom)

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

- -

RealClosedField (Real Field with the real closed axiom)

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

- -

NumClosedField (Partially ordered Closed Field with conjugation)

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

- - Over these structures, we have the following operations - `|x| == norm of x. - x <= y <=> x is less than or equal to y (:= '|y - x| == y - x). - x < y <=> x is less than y (:= (x <= y) && (x != y)). - x <= y ?= iff C <-> x is less than y, or equal iff C is true. - Num.sg x == sign of x: equal to 0 iff x = 0, to 1 iff x > 0, and - to -1 in all other cases (including x < 0). - x \is a Num.pos <=> x is positive (:= x > 0). - x \is a Num.neg <=> x is negative (:= x < 0). - x \is a Num.nneg <=> x is positive or 0 (:= x >= 0). - x \is a Num.real <=> x is real (:= x >= 0 or x < 0). - Num.min x y == minimum of x y - Num.max x y == maximum of x y - Num.bound x == in archimedean fields, and upper bound for x, i.e., - and n such that `|x| < n%:R. - Num.sqrt x == in a real-closed field, a positive square root of x if - x >= 0, or 0 otherwise. - For numeric algebraically closed fields we provide the generic definitions - 'i == the imaginary number (:= sqrtC (-1)). - 'Re z == the real component of z. - 'Im z == the imaginary component of z. - z^* == the complex conjugate of z (:= conjC z). - sqrtC z == a nonnegative square root of z, i.e., 0 <= sqrt x if 0 <= x. - n.-root z == more generally, for n > 0, an nth root of z, chosen with a - minimal non-negative argument for n > 1 (i.e., with a - maximal real part subject to a nonnegative imaginary part). - Note that n.-root (-1) is a primitive 2nth root of unity, - an thus not equal to -1 for n odd > 1 (this will be shown in - file cyclotomic.v). - -

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

- -

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

- -

- - [arg minr(i < i0 | P) M] == a value i : T minimizing M : R, subject - to the condition P (i may appear in P and M), and - provided P holds for i0. - [arg maxr(i > i0 | P) M] == a value i maximizing M subject to P and - provided P holds for i0. - [arg minr(i < i0 in A) M] == an i \in A minimizing M if i0 \in A. - [arg maxr(i > i0 in A) M] == an i \in A maximizing M if i0 \in A. - [arg minr(i < i0) M] == an i : T minimizing M, given i0 : T. - [arg maxr(i > i0) M] == an i : T maximizing M, given i0 : T. -

- -
-Set Implicit Arguments.
- -
-Local Open Scope ring_scope.
-Import GRing.Theory.
- -
-Reserved Notation "<= y" (at level 35).
-Reserved Notation ">= y" (at level 35).
-Reserved Notation "< y" (at level 35).
-Reserved Notation "> y" (at level 35).
-Reserved Notation "<= y :> T" (at level 35, y at next level).
-Reserved Notation ">= y :> T" (at level 35, y at next level).
-Reserved Notation "< y :> T" (at level 35, y at next level).
-Reserved Notation "> y :> T" (at level 35, y at next level).
- -
-Module Num.
- -
-

- -

- Principal mixin; further classes add axioms rather than operations. -

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

- -

- Base interface. -

-Module NumDomain.
- -
-Section ClassDef.
- -
-Record class_of T := Class {
-  base : GRing.IntegralDomain.class_of T;
-  mixin : mixin_of (ring_for T base)
-}.
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition clone c of phant_id class c := @Pack T c.
-Definition pack b0 (m0 : mixin_of (ring_for T b0)) :=
-  fun bT b & phant_id (GRing.IntegralDomain.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass.
-Definition ringType := @GRing.Ring.Pack cT xclass.
-Definition comRingType := @GRing.ComRing.Pack cT xclass.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> GRing.IntegralDomain.class_of.
-Coercion mixin : class_of >-> mixin_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> GRing.Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> GRing.Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> GRing.ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> GRing.UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> GRing.IntegralDomain.type.
-Canonical idomainType.
-Notation numDomainType := type.
-Notation NumMixin := Mixin.
-Notation NumDomainType T m := (@pack T _ m _ _ id _ id).
-Notation "[ 'numDomainType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'numDomainType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'numDomainType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'numDomainType' 'of' T ]") : form_scope.
-End Exports.
- -
-End NumDomain.
-Import NumDomain.Exports.
- -
-Module Import Def. Section Def.
-Import NumDomain.
-Context {R : type}.
-Implicit Types (x y : R) (C : bool).
- -
-Definition normr : R → R := norm_op (class R).
-Definition ler : rel R := le_op (class R).
-Definition ltr : rel R := lt_op (class R).
- -
-Definition ger : simpl_rel R := [rel x y | y ≤ x ].
-Definition gtr : simpl_rel R := [rel x y | y < x ].
-Definition lerif x y C : Prop := ((x ≤ y ) × ((x == y ) = C ))%type.
-Definition sgr x : R := if x == 0 then 0 else if x < 0 then -1 else 1.
-Definition minr x y : R := if x ≤ y then x else y.
-Definition maxr x y : R := if y ≤ x then x else y.
- -
-Definition Rpos : qualifier 0 R := [qualify x : R | 0 < x ].
-Definition Rneg : qualifier 0 R := [qualify x : R | x < 0].
-Definition Rnneg : qualifier 0 R := [qualify x : R | 0 ≤ x ].
-Definition Rreal : qualifier 0 R := [qualify x : R | (0 ≤ x ) || (x ≤ 0)].
-End Def. End Def.
- -
-

- -

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

-Notation norm := normr.
-Notation le := ler.
-Notation lt := ltr.
-Notation ge := ger.
-Notation gt := gtr.
-Notation sg := sgr.
-Notation max := maxr.
-Notation min := minr.
-Notation pos := Rpos.
-Notation neg := Rneg.
-Notation nneg := Rnneg.
-Notation real := Rreal.
- -
-Module Keys. Section Keys.
-Variable R : numDomainType.
-Fact Rpos_key : pred_key (@pos R).
-Definition Rpos_keyed := KeyedQualifier Rpos_key.
-Fact Rneg_key : pred_key (@real R).
-Definition Rneg_keyed := KeyedQualifier Rneg_key.
-Fact Rnneg_key : pred_key (@nneg R).
-Definition Rnneg_keyed := KeyedQualifier Rnneg_key.
-Fact Rreal_key : pred_key (@real R).
-Definition Rreal_keyed := KeyedQualifier Rreal_key.
-Definition ler_of_leif x y C (le_xy : @lerif R x y C) := le_xy .1 : le x y.
-End Keys. End Keys.
- -
-

- -

- (Exported) symbolic syntax. -

-Module Import Syntax.
-Import Def Keys.
- -
-Notation "`| x |" := (norm x) : ring_scope.
- -
-Notation "<%R" := lt : ring_scope.
-Notation ">%R" := gt : ring_scope.
-Notation "<=%R" := le : ring_scope.
-Notation ">=%R" := ge : ring_scope.
-Notation "<?=%R" := lerif : ring_scope.
- -
-Notation "< y" := (gt y) : ring_scope.
-Notation "< y :> T" := (< (y : T)) : ring_scope.
-Notation "> y" := (lt y) : ring_scope.
-Notation "> y :> T" := (> (y : T)) : ring_scope.
- -
-Notation "<= y" := (ge y) : ring_scope.
-Notation "<= y :> T" := (≤ (y : T)) : ring_scope.
-Notation ">= y" := (le y) : ring_scope.
-Notation ">= y :> T" := (≥ (y : T)) : ring_scope.
- -
-Notation "x < y" := (lt x y) : ring_scope.
-Notation "x < y :> T" := ((x : T) < (y : T)) : ring_scope.
-Notation "x > y" := (y < x) (only parsing) : ring_scope.
-Notation "x > y :> T" := ((x : T) > (y : T)) (only parsing) : ring_scope.
- -
-Notation "x <= y" := (le x y) : ring_scope.
-Notation "x <= y :> T" := ((x : T) ≤ (y : T)) : ring_scope.
-Notation "x >= y" := (y ≤ x) (only parsing) : ring_scope.
-Notation "x >= y :> T" := ((x : T) ≥ (y : T)) (only parsing) : ring_scope.
- -
-Notation "x <= y <= z" := ((x ≤ y) && (y ≤ z)) : ring_scope.
-Notation "x < y <= z" := ((x < y) && (y ≤ z)) : ring_scope.
-Notation "x <= y < z" := ((x ≤ y) && (y < z)) : ring_scope.
-Notation "x < y < z" := ((x < y) && (y < z)) : ring_scope.
- -
-Notation "x <= y ?= 'iff' C" := (lerif x y C) : ring_scope.
-Notation "x <= y ?= 'iff' C :> R" := ((x : R) ≤ (y : R) ?= iff C)
-  (only parsing) : ring_scope.
- -
-Coercion ler_of_leif : lerif >-> is_true.
- -
-Canonical Rpos_keyed.
-Canonical Rneg_keyed.
-Canonical Rnneg_keyed.
-Canonical Rreal_keyed.
- -
-End Syntax.
- -
-Section ExtensionAxioms.
- -
-Variable R : numDomainType.
- -
-Definition real_axiom : Prop := ∀ x : R, x \is real.
- -
-Definition archimedean_axiom : Prop := ∀ x : R, ∃ ub, `|x | < ub %:R.
- -
-Definition real_closed_axiom : Prop :=
-  ∀ (p : {poly R }) (a b : R),
-    a ≤ b → p .[a ] ≤ 0 ≤ p .[b ] → exists2 x, a ≤ x ≤ b & root p x.
- -
-End ExtensionAxioms.
- -
- -
-

- -

- The rest of the numbers interface hierarchy. -

-Module NumField.
- -
-Section ClassDef.
- -
-Record class_of R :=
-  Class { base : GRing.Field.class_of R; mixin : mixin_of (ring_for R base) }.
-Definition base2 R (c : class_of R) := NumDomain.Class (mixin c).
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack :=
-  fun bT b & phant_id (GRing.Field.class bT) (b : GRing.Field.class_of T) ⇒
-  fun mT m & phant_id (NumDomain.class mT) (@NumDomain.Class T b m) ⇒
-  Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass.
-Definition ringType := @GRing.Ring.Pack cT xclass.
-Definition comRingType := @GRing.ComRing.Pack cT xclass.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
-Definition numDomainType := @NumDomain.Pack cT xclass.
-Definition fieldType := @GRing.Field.Pack cT xclass.
-Definition join_numDomainType := @NumDomain.Pack fieldType xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> GRing.Field.class_of.
-Coercion base2 : class_of >-> NumDomain.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> GRing.Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> GRing.Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> GRing.ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> GRing.UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> GRing.IntegralDomain.type.
-Canonical idomainType.
-Coercion numDomainType : type >-> NumDomain.type.
-Canonical numDomainType.
-Coercion fieldType : type >-> GRing.Field.type.
-Canonical fieldType.
-Canonical join_numDomainType.
-Notation numFieldType := type.
-Notation "[ 'numFieldType' 'of' T ]" := (@pack T _ _ id _ _ id)
-  (at level 0, format "[ 'numFieldType' 'of' T ]") : form_scope.
-End Exports.
- -
-End NumField.
-Import NumField.Exports.
- -
-Module ClosedField.
- -
-Section ClassDef.
- -
-Record imaginary_mixin_of (R : numDomainType) := ImaginaryMixin {
-  imaginary : R;
-  conj_op : {rmorphism R → R };
-  _ : imaginary ^+ 2 = - 1;
-  _ : ∀ x, x × conj_op x = `|x | ^+ 2;
-}.
- -
-Record class_of R := Class {
-  base : GRing.ClosedField.class_of R;
-  mixin : mixin_of (ring_for R base);
-  conj_mixin : imaginary_mixin_of (num_for R (NumDomain.Class mixin))
-}.
-Definition base2 R (c : class_of R) := NumField.Class (mixin c).
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack :=
-  fun bT b & phant_id (GRing.ClosedField.class bT)
-                      (b : GRing.ClosedField.class_of T) ⇒
-  fun mT m & phant_id (NumField.class mT) (@NumField.Class T b m) ⇒
-  fun mc ⇒ Pack (@Class T b m mc).
-Definition clone := fun b & phant_id class (b : class_of T) ⇒ Pack b.
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass.
-Definition ringType := @GRing.Ring.Pack cT xclass.
-Definition comRingType := @GRing.ComRing.Pack cT xclass.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
-Definition numDomainType := @NumDomain.Pack cT xclass.
-Definition fieldType := @GRing.Field.Pack cT xclass.
-Definition numFieldType := @NumField.Pack cT xclass.
-Definition decFieldType := @GRing.DecidableField.Pack cT xclass.
-Definition closedFieldType := @GRing.ClosedField.Pack cT xclass.
-Definition join_dec_numDomainType := @NumDomain.Pack decFieldType xclass.
-Definition join_dec_numFieldType := @NumField.Pack decFieldType xclass.
-Definition join_numDomainType := @NumDomain.Pack closedFieldType xclass.
-Definition join_numFieldType := @NumField.Pack closedFieldType xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> GRing.ClosedField.class_of.
-Coercion base2 : class_of >-> NumField.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> GRing.Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> GRing.Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> GRing.ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> GRing.UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> GRing.IntegralDomain.type.
-Canonical idomainType.
-Coercion numDomainType : type >-> NumDomain.type.
-Canonical numDomainType.
-Coercion fieldType : type >-> GRing.Field.type.
-Canonical fieldType.
-Coercion decFieldType : type >-> GRing.DecidableField.type.
-Canonical decFieldType.
-Coercion numFieldType : type >-> NumField.type.
-Canonical numFieldType.
-Coercion closedFieldType : type >-> GRing.ClosedField.type.
-Canonical closedFieldType.
-Canonical join_dec_numDomainType.
-Canonical join_dec_numFieldType.
-Canonical join_numDomainType.
-Canonical join_numFieldType.
-Notation numClosedFieldType := type.
-Notation NumClosedFieldType T m := (@pack T _ _ id _ _ id m).
-Notation "[ 'numClosedFieldType' 'of' T 'for' cT ]" := (@clone T cT _ id)
-  (at level 0, format "[ 'numClosedFieldType' 'of' T 'for' cT ]") :
-                                                         form_scope.
-Notation "[ 'numClosedFieldType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'numClosedFieldType' 'of' T ]") : form_scope.
-End Exports.
- -
-End ClosedField.
-Import ClosedField.Exports.
- -
-Module RealDomain.
- -
-Section ClassDef.
- -
-Record class_of R :=
-  Class {base : NumDomain.class_of R; _ : @real_axiom (num_for R base)}.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition clone c of phant_id class c := @Pack T c.
-Definition pack b0 (m0 : real_axiom (num_for T b0)) :=
-  fun bT b & phant_id (NumDomain.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass.
-Definition ringType := @GRing.Ring.Pack cT xclass.
-Definition comRingType := @GRing.ComRing.Pack cT xclass.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
-Definition numDomainType := @NumDomain.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> NumDomain.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> GRing.Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> GRing.Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> GRing.ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> GRing.UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> GRing.IntegralDomain.type.
-Canonical idomainType.
-Coercion numDomainType : type >-> NumDomain.type.
-Canonical numDomainType.
-Notation realDomainType := type.
-Notation RealDomainType T m := (@pack T _ m _ _ id _ id).
-Notation "[ 'realDomainType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'realDomainType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'realDomainType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'realDomainType' 'of' T ]") : form_scope.
-End Exports.
- -
-End RealDomain.
-Import RealDomain.Exports.
- -
-Module RealField.
- -
-Section ClassDef.
- -
-Record class_of R :=
-  Class { base : NumField.class_of R; mixin : real_axiom (num_for R base) }.
-Definition base2 R (c : class_of R) := RealDomain.Class (@mixin R c).
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition pack :=
-  fun bT b & phant_id (NumField.class bT) (b : NumField.class_of T) ⇒
-  fun mT m & phant_id (RealDomain.class mT) (@RealDomain.Class T b m) ⇒
-  Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass.
-Definition ringType := @GRing.Ring.Pack cT xclass.
-Definition comRingType := @GRing.ComRing.Pack cT xclass.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
-Definition numDomainType := @NumDomain.Pack cT xclass.
-Definition realDomainType := @RealDomain.Pack cT xclass.
-Definition fieldType := @GRing.Field.Pack cT xclass.
-Definition numFieldType := @NumField.Pack cT xclass.
-Definition join_fieldType := @GRing.Field.Pack realDomainType xclass.
-Definition join_numFieldType := @NumField.Pack realDomainType xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> NumField.class_of.
-Coercion base2 : class_of >-> RealDomain.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> GRing.Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> GRing.Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> GRing.ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> GRing.UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> GRing.IntegralDomain.type.
-Canonical idomainType.
-Coercion numDomainType : type >-> NumDomain.type.
-Canonical numDomainType.
-Coercion realDomainType : type >-> RealDomain.type.
-Canonical realDomainType.
-Coercion fieldType : type >-> GRing.Field.type.
-Canonical fieldType.
-Coercion numFieldType : type >-> NumField.type.
-Canonical numFieldType.
-Canonical join_fieldType.
-Canonical join_numFieldType.
-Notation realFieldType := type.
-Notation "[ 'realFieldType' 'of' T ]" := (@pack T _ _ id _ _ id)
-  (at level 0, format "[ 'realFieldType' 'of' T ]") : form_scope.
-End Exports.
- -
-End RealField.
-Import RealField.Exports.
- -
-Module ArchimedeanField.
- -
-Section ClassDef.
- -
-Record class_of R :=
-  Class { base : RealField.class_of R; _ : archimedean_axiom (num_for R base) }.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition clone c of phant_id class c := @Pack T c.
-Definition pack b0 (m0 : archimedean_axiom (num_for T b0)) :=
-  fun bT b & phant_id (RealField.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass.
-Definition ringType := @GRing.Ring.Pack cT xclass.
-Definition comRingType := @GRing.ComRing.Pack cT xclass.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
-Definition numDomainType := @NumDomain.Pack cT xclass.
-Definition realDomainType := @RealDomain.Pack cT xclass.
-Definition fieldType := @GRing.Field.Pack cT xclass.
-Definition numFieldType := @NumField.Pack cT xclass.
-Definition realFieldType := @RealField.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> RealField.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> GRing.Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> GRing.Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> GRing.ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> GRing.UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> GRing.IntegralDomain.type.
-Canonical idomainType.
-Coercion numDomainType : type >-> NumDomain.type.
-Canonical numDomainType.
-Coercion realDomainType : type >-> RealDomain.type.
-Canonical realDomainType.
-Coercion fieldType : type >-> GRing.Field.type.
-Canonical fieldType.
-Coercion numFieldType : type >-> NumField.type.
-Canonical numFieldType.
-Coercion realFieldType : type >-> RealField.type.
-Canonical realFieldType.
-Notation archiFieldType := type.
-Notation ArchiFieldType T m := (@pack T _ m _ _ id _ id).
-Notation "[ 'archiFieldType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'archiFieldType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'archiFieldType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'archiFieldType' 'of' T ]") : form_scope.
-End Exports.
- -
-End ArchimedeanField.
-Import ArchimedeanField.Exports.
- -
-Module RealClosedField.
- -
-Section ClassDef.
- -
-Record class_of R :=
-  Class { base : RealField.class_of R; _ : real_closed_axiom (num_for R base) }.
- -
-Structure type := Pack {sort; _ : class_of sort}.
-Variables (T : Type) (cT : type).
-Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
-Let xT := let: Pack T _ := cT in T.
-Notation xclass := (class : class_of xT).
- -
-Definition clone c of phant_id class c := @Pack T c.
-Definition pack b0 (m0 : real_closed_axiom (num_for T b0)) :=
-  fun bT b & phant_id (RealField.class bT) b ⇒
-  fun m & phant_id m0 m ⇒ Pack (@Class T b m).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @GRing.Zmodule.Pack cT xclass.
-Definition ringType := @GRing.Ring.Pack cT xclass.
-Definition comRingType := @GRing.ComRing.Pack cT xclass.
-Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
-Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
-Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
-Definition numDomainType := @NumDomain.Pack cT xclass.
-Definition realDomainType := @RealDomain.Pack cT xclass.
-Definition fieldType := @GRing.Field.Pack cT xclass.
-Definition numFieldType := @NumField.Pack cT xclass.
-Definition realFieldType := @RealField.Pack cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
-Coercion base : class_of >-> RealField.class_of.
-Coercion sort : type >-> Sortclass.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> GRing.Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> GRing.Ring.type.
-Canonical ringType.
-Coercion comRingType : type >-> GRing.ComRing.type.
-Canonical comRingType.
-Coercion unitRingType : type >-> GRing.UnitRing.type.
-Canonical unitRingType.
-Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> GRing.IntegralDomain.type.
-Canonical idomainType.
-Coercion numDomainType : type >-> NumDomain.type.
-Canonical numDomainType.
-Coercion realDomainType : type >-> RealDomain.type.
-Canonical realDomainType.
-Coercion fieldType : type >-> GRing.Field.type.
-Canonical fieldType.
-Coercion numFieldType : type >-> NumField.type.
-Canonical numFieldType.
-Coercion realFieldType : type >-> RealField.type.
-Canonical realFieldType.
-Notation rcfType := Num.RealClosedField.type.
-Notation RcfType T m := (@pack T _ m _ _ id _ id).
-Notation "[ 'rcfType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
-  (at level 0, format "[ 'rcfType' 'of' T 'for' cT ]") : form_scope.
-Notation "[ 'rcfType' 'of' T ]" := (@clone T _ _ id)
-  (at level 0, format "[ 'rcfType' 'of' T ]") : form_scope.
-End Exports.
- -
-End RealClosedField.
-Import RealClosedField.Exports.
- -
-

- -

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

-Module Import Internals.
- -
-Section Domain.
-Variable R : numDomainType.
-Implicit Types x y : R.
- -
-

- -

- Lemmas from the signature -

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

- -

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

- -
-Lemma ger0_def x : (0 ≤ x ) = (`|x | == x ).
- -
-Lemma subr_ge0 x y : (0 ≤ x - y ) = (y ≤ x ).
- -
-Lemma oppr_ge0 x : (0 ≤ - x ) = (x ≤ 0).
- -
-Lemma ler01 : 0 ≤ 1 :> R.
- -
-Lemma ltr01 : 0 < 1 :> R.
- -
-Lemma ltrW x y : x < y → x ≤ y.
- -
-Lemma lerr x : x ≤ x.
- -
-Lemma le0r x : (0 ≤ x ) = (x == 0) || (0 < x ).
- -
-Lemma addr_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
- -
-Lemma pmulr_rgt0 x y : 0 < x → (0 < x × y ) = (0 < y ).
- -
-

- -

- Closure properties of the real predicates. -

- -
-Lemma posrE x : (x \is pos ) = (0 < x ).
-Lemma nnegrE x : (x \is nneg ) = (0 ≤ x ).
-Lemma realE x : (x \is real ) = (0 ≤ x ) || (x ≤ 0).
- -
-Fact pos_divr_closed : divr_closed (@pos R).
-Canonical pos_mulrPred := MulrPred pos_divr_closed.
-Canonical pos_divrPred := DivrPred pos_divr_closed.
- -
-Fact nneg_divr_closed : divr_closed (@nneg R).
-Canonical nneg_mulrPred := MulrPred nneg_divr_closed.
-Canonical nneg_divrPred := DivrPred nneg_divr_closed.
- -
-Fact nneg_addr_closed : addr_closed (@nneg R).
- Canonical nneg_addrPred := AddrPred nneg_addr_closed.
-Canonical nneg_semiringPred := SemiringPred nneg_divr_closed.
- -
-Fact real_oppr_closed : oppr_closed (@real R).
- Canonical real_opprPred := OpprPred real_oppr_closed.
- -
-Fact real_addr_closed : addr_closed (@real R).
-Canonical real_addrPred := AddrPred real_addr_closed.
-Canonical real_zmodPred := ZmodPred real_oppr_closed.
- -
-Fact real_divr_closed : divr_closed (@real R).
-Canonical real_mulrPred := MulrPred real_divr_closed.
-Canonical real_smulrPred := SmulrPred real_divr_closed.
-Canonical real_divrPred := DivrPred real_divr_closed.
-Canonical real_sdivrPred := SdivrPred real_divr_closed.
-Canonical real_semiringPred := SemiringPred real_divr_closed.
-Canonical real_subringPred := SubringPred real_divr_closed.
-Canonical real_divringPred := DivringPred real_divr_closed.
- -
-End Domain.
- -
-Lemma num_real (R : realDomainType) (x : R) : x \is real.
- -
-Fact archi_bound_subproof (R : archiFieldType) : archimedean_axiom R.
- -
-Section RealClosed.
-Variable R : rcfType.
- -
-Lemma poly_ivt : real_closed_axiom R.
- -
-Fact sqrtr_subproof (x : R) :
- exists2 y, 0 ≤ y & (if 0 ≤ x then y ^+ 2 == x else y == 0) : bool.
- -
-End RealClosed.
- -
-End Internals.
- -
-Module PredInstances.
- -
-Canonical pos_mulrPred.
-Canonical pos_divrPred.
- -
-Canonical nneg_addrPred.
-Canonical nneg_mulrPred.
-Canonical nneg_divrPred.
-Canonical nneg_semiringPred.
- -
-Canonical real_addrPred.
-Canonical real_opprPred.
-Canonical real_zmodPred.
-Canonical real_mulrPred.
-Canonical real_smulrPred.
-Canonical real_divrPred.
-Canonical real_sdivrPred.
-Canonical real_semiringPred.
-Canonical real_subringPred.
-Canonical real_divringPred.
- -
-End PredInstances.
- -
-Module Import ExtraDef.
- -
-Definition archi_bound {R} x := sval (sigW (@archi_bound_subproof R x)).
- -
-Definition sqrtr {R} x := s2val (sig2W (@sqrtr_subproof R x)).
- -
-End ExtraDef.
- -
-Notation bound := archi_bound.
-Notation sqrt := sqrtr.
- -
-Module Theory.
- -
-Section NumIntegralDomainTheory.
- -
-Variable R : numDomainType.
-Implicit Types x y z t : R.
- -
-

- -

- Lemmas from the signature (reexported from internals). -

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

- -

- Predicate and relation definitions. -

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

- -

- General properties of <= and < -

- -
-Lemma lerr x : x ≤ x.
-Lemma ltrr x : x < x = false.
-Lemma ltrW x y : x < y → x ≤ y.
-Hint Resolve lerr ltrr ltrW : core.
- -
-Lemma ltr_neqAle x y : (x < y ) = (x != y ) && (x ≤ y ).
- -
-Lemma ler_eqVlt x y : (x ≤ y ) = (x == y ) || (x < y ).
- -
-Lemma lt0r x : (0 < x ) = (x != 0) && (0 ≤ x ).
-Lemma le0r x : (0 ≤ x ) = (x == 0) || (0 < x ).
- -
-Lemma lt0r_neq0 (x : R) : 0 < x → x != 0.
- -
-Lemma ltr0_neq0 (x : R) : x < 0 → x != 0.
- -
-Lemma gtr_eqF x y : y < x → x == y = false.
- -
-Lemma ltr_eqF x y : x < y → x == y = false.
- -
-Lemma pmulr_rgt0 x y : 0 < x → (0 < x × y ) = (0 < y ).
- -
-Lemma pmulr_rge0 x y : 0 < x → (0 ≤ x × y ) = (0 ≤ y ).
- -
-

- -

- Integer comparisons and characteristic 0. -

-Lemma ler01 : 0 ≤ 1 :> R.
-Lemma ltr01 : 0 < 1 :> R.
-Lemma ler0n n : 0 ≤ n %:R :> R.
-Hint Resolve ler01 ltr01 ler0n : core.
-Lemma ltr0Sn n : 0 < n .+1 %:R :> R.
- Lemma ltr0n n : (0 < n %:R :> R ) = (0 < n)%N.
- Hint Resolve ltr0Sn : core.
- -
-Lemma pnatr_eq0 n : (n %:R == 0 :> R ) = (n == 0)%N.
- -
-Lemma char_num : [char R ] =i pred0.
- -
-

- -

- Properties of the norm. -

- -
-Lemma ger0_def x : (0 ≤ x ) = (`|x | == x ).
-Lemma normr_idP {x} : reflect (`|x | = x) (0 ≤ x).
- Lemma ger0_norm x : 0 ≤ x → `|x | = x.
- -
-Lemma normr0 : `|0| = 0 :> R.
-Lemma normr1 : `|1| = 1 :> R.
-Lemma normr_nat n : `|n %:R | = n %:R :> R.
-Lemma normrMn x n : `|x *+ n | = `|x | *+ n.
- -
-Lemma normr_prod I r (P : pred I) (F : I → R) :
- `|\prod_(i <- r | P i ) F i | = \prod_(i <- r | P i ) `|F i |.
- -
-Lemma normrX n x : `|x ^+ n | = `|x | ^+ n.
- -
-Lemma normr_unit : {homo (@norm R ) : x / x \is a GRing.unit }.
- -
-Lemma normrV : {in GRing.unit , {morph (@normr R ) : x / x ^-1 }}.
- -
-Lemma normr0P {x} : reflect (`|x | = 0) (x == 0).
- -
-Definition normr_eq0 x := sameP (`|x | =P 0) normr0P.
- -
-Lemma normrN1 : `|-1| = 1 :> R.
- -
-Lemma normrN x : `|- x | = `|x |.
- -
-Lemma distrC x y : `|x - y | = `|y - x |.
- -
-Lemma ler0_def x : (x ≤ 0) = (`|x | == - x ).
- -
-Lemma normr_id x : `|`|x | | = `|x |.
- -
-Lemma normr_ge0 x : 0 ≤ `|x |.
-Hint Resolve normr_ge0 : core.
- -
-Lemma ler0_norm x : x ≤ 0 → `|x | = - x.
- -
-Definition gtr0_norm x (hx : 0 < x) := ger0_norm (ltrW hx).
-Definition ltr0_norm x (hx : x < 0) := ler0_norm (ltrW hx).
- -
-

- -

- Comparision to 0 of a difference -

- -
-Lemma subr_ge0 x y : (0 ≤ y - x ) = (x ≤ y ).
-Lemma subr_gt0 x y : (0 < y - x ) = (x < y ).
- Lemma subr_le0 x y : (y - x ≤ 0) = (y ≤ x ).
- Lemma subr_lt0 x y : (y - x < 0) = (y < x ).
- -
-Definition subr_lte0 := (subr_le0 , subr_lt0 ).
-Definition subr_gte0 := (subr_ge0 , subr_gt0 ).
-Definition subr_cp0 := (subr_lte0 , subr_gte0 ).
- -
-

- -

- Ordered ring properties. -

- -
-Lemma ler_asym : antisymmetric (<=%R : rel R).
- -
-Lemma eqr_le x y : (x == y ) = (x ≤ y ≤ x ).
- -
-Lemma ltr_trans : transitive (@ltr R).
- -
-Lemma ler_lt_trans y x z : x ≤ y → y < z → x < z.
- -
-Lemma ltr_le_trans y x z : x < y → y ≤ z → x < z.
- -
-Lemma ler_trans : transitive (@ler R).
- -
-Definition lter01 := (ler01 , ltr01 ).
-Definition lterr := (lerr , ltrr ).
- -
-Lemma addr_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
- -
-Lemma lerifP x y C : reflect (x ≤ y ?= iff C) (if C then x == y else x < y).
- -
-Lemma ltr_asym x y : x < y < x = false.
- -
-Lemma ler_anti : antisymmetric (@ler R).
- -
-Lemma ltr_le_asym x y : x < y ≤ x = false.
- -
-Lemma ler_lt_asym x y : x ≤ y < x = false.
- -
-Definition lter_anti := (=^~ eqr_le , ltr_asym , ltr_le_asym , ler_lt_asym ).
- -
-Lemma ltr_geF x y : x < y → (y ≤ x = false ).
- -
-Lemma ler_gtF x y : x ≤ y → (y < x = false ).
- -
-Definition ltr_gtF x y hxy := ler_gtF (@ltrW x y hxy).
- -
-

- -

- Norm and order properties. -

- -
-Lemma normr_le0 x : (`|x | ≤ 0) = (x == 0).
- -
-Lemma normr_lt0 x : `|x | < 0 = false.
- -
-Lemma normr_gt0 x : (`|x | > 0) = (x != 0).
- -
-Definition normrE x := (normr_id , normr0 , normr1 , normrN1 , normr_ge0 , normr_eq0 ,
- normr_lt0 , normr_le0 , normr_gt0 , normrN ).
- -
-End NumIntegralDomainTheory.
- -
-Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0 : core.
- -
-Section NumIntegralDomainMonotonyTheory.
- -
-Variables R R' : numDomainType.
-Implicit Types m n p : nat.
-Implicit Types x y z : R.
-Implicit Types u v w : R'.
- -
-

- -

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

- -
-Let leqnn := leqnn.
-Let ltnE := ltn_neqAle.
-Let ltrE := @ltr_neqAle R.
-Let ltr'E := @ltr_neqAle R'.
-Let gtnE (m n : nat) : (m > n)%N = (m != n ) && (m ≥ n)%N.
- Let gtrE (x y : R) : (x > y ) = (x != y ) && (x ≥ y ).
- Let gtr'E (x y : R') : (x > y ) = (x != y ) && (x ≥ y ).
- Let leq_anti : antisymmetric leq.
- Let geq_anti : antisymmetric geq.
- Let ler_antiR := @ler_anti R.
-Let ler_antiR' := @ler_anti R'.
-Let ger_antiR : antisymmetric (>=%R : rel R).
- Let ger_antiR' : antisymmetric (>=%R : rel R').
- Let leq_total := leq_total.
-Let geq_total : total geq.
- -
-Section AcrossTypes.
- -
-Variables (D D' : {pred R }) (f : R → R').
- -
-Lemma ltrW_homo : {homo f : x y / x < y } → {homo f : x y / x ≤ y }.
- -
-Lemma ltrW_nhomo : {homo f : x y /~ x < y } → {homo f : x y /~ x ≤ y }.
- -
-Lemma inj_homo_ltr :
- injective f → {homo f : x y / x ≤ y } → {homo f : x y / x < y }.
- -
-Lemma inj_nhomo_ltr :
- injective f → {homo f : x y /~ x ≤ y } → {homo f : x y /~ x < y }.
- -
-Lemma incr_inj : {mono f : x y / x ≤ y } → injective f.
- -
-Lemma decr_inj : {mono f : x y /~ x ≤ y } → injective f.
- -
-Lemma lerW_mono : {mono f : x y / x ≤ y } → {mono f : x y / x < y }.
- -
-Lemma lerW_nmono : {mono f : x y /~ x ≤ y } → {mono f : x y /~ x < y }.
- -
-

- -

- Monotony in D D' -

-Lemma ltrW_homo_in :
-  {in D & D', {homo f : x y / x < y }} → {in D & D', {homo f : x y / x ≤ y }}.
- -
-Lemma ltrW_nhomo_in :
-  {in D & D', {homo f : x y /~ x < y }} → {in D & D', {homo f : x y /~ x ≤ y }}.
- -
-Lemma inj_homo_ltr_in :
-    {in D & D', injective f } → {in D & D', {homo f : x y / x ≤ y }} →
-  {in D & D', {homo f : x y / x < y }}.
- -
-Lemma inj_nhomo_ltr_in :
-    {in D & D', injective f } → {in D & D', {homo f : x y /~ x ≤ y }} →
-  {in D & D', {homo f : x y /~ x < y }}.
- -
-Lemma incr_inj_in : {in D &, {mono f : x y / x ≤ y }} →
-   {in D &, injective f }.
- -
-Lemma decr_inj_in :
-  {in D &, {mono f : x y /~ x ≤ y }} → {in D &, injective f }.
- -
-Lemma lerW_mono_in :
-  {in D &, {mono f : x y / x ≤ y }} → {in D &, {mono f : x y / x < y }}.
- -
-Lemma lerW_nmono_in :
-  {in D &, {mono f : x y /~ x ≤ y }} → {in D &, {mono f : x y /~ x < y }}.
- -
-End AcrossTypes.
- -
-Section NatToR.
- -
-Variables (D D' : {pred nat }) (f : nat → R).
- -
-Lemma ltnrW_homo : {homo f : m n / (m < n)%N >-> m < n } →
-  {homo f : m n / (m ≤ n)%N >-> m ≤ n }.
- -
-Lemma ltnrW_nhomo : {homo f : m n / (n < m)%N >-> m < n } →
-  {homo f : m n / (n ≤ m)%N >-> m ≤ n }.
- -
-Lemma inj_homo_ltnr : injective f →
-  {homo f : m n / (m ≤ n)%N >-> m ≤ n } →
-  {homo f : m n / (m < n)%N >-> m < n }.
- -
-Lemma inj_nhomo_ltnr : injective f →
-  {homo f : m n / (n ≤ m)%N >-> m ≤ n } →
-  {homo f : m n / (n < m)%N >-> m < n }.
- -
-Lemma incnr_inj : {mono f : m n / (m ≤ n)%N >-> m ≤ n } → injective f.
- -
-Lemma decnr_inj_inj : {mono f : m n / (n ≤ m)%N >-> m ≤ n } → injective f.
- -
-Lemma lenrW_mono : {mono f : m n / (m ≤ n)%N >-> m ≤ n } →
-  {mono f : m n / (m < n)%N >-> m < n }.
- -
-Lemma lenrW_nmono : {mono f : m n / (n ≤ m)%N >-> m ≤ n } →
-  {mono f : m n / (n < m)%N >-> m < n }.
- -
-Lemma lenr_mono : {homo f : m n / (m < n)%N >-> m < n } →
-   {mono f : m n / (m ≤ n)%N >-> m ≤ n }.
- -
-Lemma lenr_nmono : {homo f : m n / (n < m)%N >-> m < n } →
-  {mono f : m n / (n ≤ m)%N >-> m ≤ n }.
- -
-Lemma ltnrW_homo_in : {in D & D', {homo f : m n / (m < n)%N >-> m < n }} →
-  {in D & D', {homo f : m n / (m ≤ n)%N >-> m ≤ n }}.
- -
-Lemma ltnrW_nhomo_in : {in D & D', {homo f : m n / (n < m)%N >-> m < n }} →
-  {in D & D', {homo f : m n / (n ≤ m)%N >-> m ≤ n }}.
- -
-Lemma inj_homo_ltnr_in : {in D & D', injective f } →
-  {in D & D', {homo f : m n / (m ≤ n)%N >-> m ≤ n }} →
-  {in D & D', {homo f : m n / (m < n)%N >-> m < n }}.
- -
-Lemma inj_nhomo_ltnr_in : {in D & D', injective f } →
-  {in D & D', {homo f : m n / (n ≤ m)%N >-> m ≤ n }} →
-  {in D & D', {homo f : m n / (n < m)%N >-> m < n }}.
- -
-Lemma incnr_inj_in : {in D &, {mono f : m n / (m ≤ n)%N >-> m ≤ n }} →
-  {in D &, injective f }.
- -
-Lemma decnr_inj_inj_in : {in D &, {mono f : m n / (n ≤ m)%N >-> m ≤ n }} →
-  {in D &, injective f }.
- -
-Lemma lenrW_mono_in : {in D &, {mono f : m n / (m ≤ n)%N >-> m ≤ n }} →
-  {in D &, {mono f : m n / (m < n)%N >-> m < n }}.
- -
-Lemma lenrW_nmono_in : {in D &, {mono f : m n / (n ≤ m)%N >-> m ≤ n }} →
-  {in D &, {mono f : m n / (n < m)%N >-> m < n }}.
- -
-Lemma lenr_mono_in : {in D &, {homo f : m n / (m < n)%N >-> m < n }} →
-   {in D &, {mono f : m n / (m ≤ n)%N >-> m ≤ n }}.
- -
-Lemma lenr_nmono_in : {in D &, {homo f : m n / (n < m)%N >-> m < n }} →
-  {in D &, {mono f : m n / (n ≤ m)%N >-> m ≤ n }}.
- -
-End NatToR.
- -
-Section RToNat.
- -
-Variables (D D' : {pred R }) (f : R → nat).
- -
-Lemma ltrnW_homo : {homo f : m n / m < n >-> (m < n)%N} →
-  {homo f : m n / m ≤ n >-> (m ≤ n)%N}.
- -
-Lemma ltrnW_nhomo : {homo f : m n / n < m >-> (m < n)%N} →
-  {homo f : m n / n ≤ m >-> (m ≤ n)%N}.
- -
-Lemma inj_homo_ltrn : injective f →
-  {homo f : m n / m ≤ n >-> (m ≤ n)%N} →
-  {homo f : m n / m < n >-> (m < n)%N}.
- -
-Lemma inj_nhomo_ltrn : injective f →
-  {homo f : m n / n ≤ m >-> (m ≤ n)%N} →
-  {homo f : m n / n < m >-> (m < n)%N}.
- -
-Lemma incrn_inj : {mono f : m n / m ≤ n >-> (m ≤ n)%N} → injective f.
- -
-Lemma decrn_inj : {mono f : m n / n ≤ m >-> (m ≤ n)%N} → injective f.
- -
-Lemma lernW_mono : {mono f : m n / m ≤ n >-> (m ≤ n)%N} →
-  {mono f : m n / m < n >-> (m < n)%N}.
- -
-Lemma lernW_nmono : {mono f : m n / n ≤ m >-> (m ≤ n)%N} →
-  {mono f : m n / n < m >-> (m < n)%N}.
- -
-Lemma ltrnW_homo_in : {in D & D', {homo f : m n / m < n >-> (m < n)%N}} →
-  {in D & D', {homo f : m n / m ≤ n >-> (m ≤ n)%N}}.
- -
-Lemma ltrnW_nhomo_in : {in D & D', {homo f : m n / n < m >-> (m < n)%N}} →
-  {in D & D', {homo f : m n / n ≤ m >-> (m ≤ n)%N}}.
- -
-Lemma inj_homo_ltrn_in : {in D & D', injective f } →
-  {in D & D', {homo f : m n / m ≤ n >-> (m ≤ n)%N}} →
-  {in D & D', {homo f : m n / m < n >-> (m < n)%N}}.
- -
-Lemma inj_nhomo_ltrn_in : {in D & D', injective f } →
-  {in D & D', {homo f : m n / n ≤ m >-> (m ≤ n)%N}} →
-  {in D & D', {homo f : m n / n < m >-> (m < n)%N}}.
- -
-Lemma incrn_inj_in : {in D &, {mono f : m n / m ≤ n >-> (m ≤ n)%N}} →
-  {in D &, injective f }.
- -
-Lemma decrn_inj_in : {in D &, {mono f : m n / n ≤ m >-> (m ≤ n)%N}} →
-  {in D &, injective f }.
- -
-Lemma lernW_mono_in : {in D &, {mono f : m n / m ≤ n >-> (m ≤ n)%N}} →
-  {in D &, {mono f : m n / m < n >-> (m < n)%N}}.
- -
-Lemma lernW_nmono_in : {in D &, {mono f : m n / n ≤ m >-> (m ≤ n)%N}} →
-  {in D &, {mono f : m n / n < m >-> (m < n)%N}}.
- -
-End RToNat.
- -
-End NumIntegralDomainMonotonyTheory.
- -
-Section NumDomainOperationTheory.
- -
-Variable R : numDomainType.
-Implicit Types x y z t : R.
- -
-

- -

- Comparision and opposite. -

- -
-Lemma ler_opp2 : {mono -%R : x y /~ x ≤ y :> R }.
- Hint Resolve ler_opp2 : core.
-Lemma ltr_opp2 : {mono -%R : x y /~ x < y :> R }.
- Hint Resolve ltr_opp2 : core.
-Definition lter_opp2 := (ler_opp2 , ltr_opp2 ).
- -
-Lemma ler_oppr x y : (x ≤ - y ) = (y ≤ - x ).
- -
-Lemma ltr_oppr x y : (x < - y ) = (y < - x ).
- -
-Definition lter_oppr := (ler_oppr , ltr_oppr ).
- -
-Lemma ler_oppl x y : (- x ≤ y ) = (- y ≤ x ).
- -
-Lemma ltr_oppl x y : (- x < y ) = (- y < x ).
- -
-Definition lter_oppl := (ler_oppl , ltr_oppl ).
- -
-Lemma oppr_ge0 x : (0 ≤ - x ) = (x ≤ 0).
- -
-Lemma oppr_gt0 x : (0 < - x ) = (x < 0).
- -
-Definition oppr_gte0 := (oppr_ge0 , oppr_gt0 ).
- -
-Lemma oppr_le0 x : (- x ≤ 0) = (0 ≤ x ).
- -
-Lemma oppr_lt0 x : (- x < 0) = (0 < x ).
- -
-Definition oppr_lte0 := (oppr_le0 , oppr_lt0 ).
-Definition oppr_cp0 := (oppr_gte0 , oppr_lte0 ).
-Definition lter_oppE := (oppr_cp0 , lter_opp2 ).
- -
-Lemma ge0_cp x : 0 ≤ x → (- x ≤ 0) × (- x ≤ x ).
- -
-Lemma gt0_cp x : 0 < x →
- (0 ≤ x ) × (- x ≤ 0) × (- x ≤ x ) × (- x < 0) × (- x < x ).
- -
-Lemma le0_cp x : x ≤ 0 → (0 ≤ - x ) × (x ≤ - x ).
- -
-Lemma lt0_cp x :
- x < 0 → (x ≤ 0) × (0 ≤ - x ) × (x ≤ - x ) × (0 < - x ) × (x < - x ).
- -
-

- -

- Properties of the real subset. -

- -
-Lemma ger0_real x : 0 ≤ x → x \is real.
- -
-Lemma ler0_real x : x ≤ 0 → x \is real.
- -
-Lemma gtr0_real x : 0 < x → x \is real.
- -
-Lemma ltr0_real x : x < 0 → x \is real.
- -
-Lemma real0 : 0 \is @real R.
-Hint Resolve real0 : core.
- -
-Lemma real1 : 1 \is @real R.
-Hint Resolve real1 : core.
- -
-Lemma realn n : n %:R \is @real R.
- -
-Lemma ler_leVge x y : x ≤ 0 → y ≤ 0 → (x ≤ y ) || (y ≤ x ).
- -
-Lemma real_leVge x y : x \is real → y \is real → (x ≤ y ) || (y ≤ x ).
- -
-Lemma realB : {in real &, ∀ x y, x - y \is real }.
- -
-Lemma realN : {mono (@GRing.opp R ) : x / x \is real }.
- -
-

- -

- :TODO: add a rpredBC in ssralg -

-Lemma realBC x y : (x - y \is real ) = (y - x \is real ).
- -
-Lemma realD : {in real &, ∀ x y, x + y \is real }.
- -
-

- -

- dichotomy and trichotomy -

- -

- real wlog -

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

- -

- Monotony of addition -

-Lemma ler_add2l x : {mono +%R x : y z / y ≤ z }.
- -
-Lemma ler_add2r x : {mono +%R ^~ x : y z / y ≤ z }.
- -
-Lemma ltr_add2l x : {mono +%R x : y z / y < z }.
- -
-Lemma ltr_add2r x : {mono +%R ^~ x : y z / y < z }.
- -
-Definition ler_add2 := (ler_add2l , ler_add2r ).
-Definition ltr_add2 := (ltr_add2l , ltr_add2r ).
-Definition lter_add2 := (ler_add2 , ltr_add2 ).
- -
-

- -

- Addition, subtraction and transitivity -

-Lemma ler_add x y z t : x ≤ y → z ≤ t → x + z ≤ y + t.
- -
-Lemma ler_lt_add x y z t : x ≤ y → z < t → x + z < y + t.
- -
-Lemma ltr_le_add x y z t : x < y → z ≤ t → x + z < y + t.
- -
-Lemma ltr_add x y z t : x < y → z < t → x + z < y + t.
- -
-Lemma ler_sub x y z t : x ≤ y → t ≤ z → x - z ≤ y - t.
- -
-Lemma ler_lt_sub x y z t : x ≤ y → t < z → x - z < y - t.
- -
-Lemma ltr_le_sub x y z t : x < y → t ≤ z → x - z < y - t.
- -
-Lemma ltr_sub x y z t : x < y → t < z → x - z < y - t.
- -
-Lemma ler_subl_addr x y z : (x - y ≤ z ) = (x ≤ z + y ).
- -
-Lemma ltr_subl_addr x y z : (x - y < z ) = (x < z + y ).
- -
-Lemma ler_subr_addr x y z : (x ≤ y - z ) = (x + z ≤ y ).
- -
-Lemma ltr_subr_addr x y z : (x < y - z ) = (x + z < y ).
- -
-Definition ler_sub_addr := (ler_subl_addr , ler_subr_addr ).
-Definition ltr_sub_addr := (ltr_subl_addr , ltr_subr_addr ).
-Definition lter_sub_addr := (ler_sub_addr , ltr_sub_addr ).
- -
-Lemma ler_subl_addl x y z : (x - y ≤ z ) = (x ≤ y + z ).
- -
-Lemma ltr_subl_addl x y z : (x - y < z ) = (x < y + z ).
- -
-Lemma ler_subr_addl x y z : (x ≤ y - z ) = (z + x ≤ y ).
- -
-Lemma ltr_subr_addl x y z : (x < y - z ) = (z + x < y ).
- -
-Definition ler_sub_addl := (ler_subl_addl , ler_subr_addl ).
-Definition ltr_sub_addl := (ltr_subl_addl , ltr_subr_addl ).
-Definition lter_sub_addl := (ler_sub_addl , ltr_sub_addl ).
- -
-Lemma ler_addl x y : (x ≤ x + y ) = (0 ≤ y ).
- -
-Lemma ltr_addl x y : (x < x + y ) = (0 < y ).
- -
-Lemma ler_addr x y : (x ≤ y + x ) = (0 ≤ y ).
- -
-Lemma ltr_addr x y : (x < y + x ) = (0 < y ).
- -
-Lemma ger_addl x y : (x + y ≤ x ) = (y ≤ 0).
- -
-Lemma gtr_addl x y : (x + y < x ) = (y < 0).
- -
-Lemma ger_addr x y : (y + x ≤ x ) = (y ≤ 0).
- -
-Lemma gtr_addr x y : (y + x < x ) = (y < 0).
- -
-Definition cpr_add := (ler_addl , ler_addr , ger_addl , ger_addl ,
- ltr_addl , ltr_addr , gtr_addl , gtr_addl ).
- -
-

- -

- Addition with left member knwon to be positive/negative -

-Lemma ler_paddl y x z : 0 ≤ x → y ≤ z → y ≤ x + z.
- -
-Lemma ltr_paddl y x z : 0 ≤ x → y < z → y < x + z.
- -
-Lemma ltr_spaddl y x z : 0 < x → y ≤ z → y < x + z.
- -
-Lemma ltr_spsaddl y x z : 0 < x → y < z → y < x + z.
- -
-Lemma ler_naddl y x z : x ≤ 0 → y ≤ z → x + y ≤ z.
- -
-Lemma ltr_naddl y x z : x ≤ 0 → y < z → x + y < z.
- -
-Lemma ltr_snaddl y x z : x < 0 → y ≤ z → x + y < z.
- -
-Lemma ltr_snsaddl y x z : x < 0 → y < z → x + y < z.
- -
-

- -

- Addition with right member we know positive/negative -

-Lemma ler_paddr y x z : 0 ≤ x → y ≤ z → y ≤ z + x.
- -
-Lemma ltr_paddr y x z : 0 ≤ x → y < z → y < z + x.
- -
-Lemma ltr_spaddr y x z : 0 < x → y ≤ z → y < z + x.
- -
-Lemma ltr_spsaddr y x z : 0 < x → y < z → y < z + x.
- -
-Lemma ler_naddr y x z : x ≤ 0 → y ≤ z → y + x ≤ z.
- -
-Lemma ltr_naddr y x z : x ≤ 0 → y < z → y + x < z.
- -
-Lemma ltr_snaddr y x z : x < 0 → y ≤ z → y + x < z.
- -
-Lemma ltr_snsaddr y x z : x < 0 → y < z → y + x < z.
- -
-

- -

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

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

- -

- big sum and ler -

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

- -

- :TODO: Cyril : See which form to keep -

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

- -

- mulr and ler/ltr -

- -
-Lemma ler_pmul2l x : 0 < x → {mono *%R x : x y / x ≤ y }.
- -
-Lemma ltr_pmul2l x : 0 < x → {mono *%R x : x y / x < y }.
- -
-Definition lter_pmul2l := (ler_pmul2l , ltr_pmul2l ).
- -
-Lemma ler_pmul2r x : 0 < x → {mono *%R ^~ x : x y / x ≤ y }.
- -
-Lemma ltr_pmul2r x : 0 < x → {mono *%R ^~ x : x y / x < y }.
- -
-Definition lter_pmul2r := (ler_pmul2r , ltr_pmul2r ).
- -
-Lemma ler_nmul2l x : x < 0 → {mono *%R x : x y /~ x ≤ y }.
- -
-Lemma ltr_nmul2l x : x < 0 → {mono *%R x : x y /~ x < y }.
- -
-Definition lter_nmul2l := (ler_nmul2l , ltr_nmul2l ).
- -
-Lemma ler_nmul2r x : x < 0 → {mono *%R ^~ x : x y /~ x ≤ y }.
- -
-Lemma ltr_nmul2r x : x < 0 → {mono *%R ^~ x : x y /~ x < y }.
- -
-Definition lter_nmul2r := (ler_nmul2r , ltr_nmul2r ).
- -
-Lemma ler_wpmul2l x : 0 ≤ x → {homo *%R x : y z / y ≤ z }.
- -
-Lemma ler_wpmul2r x : 0 ≤ x → {homo *%R ^~ x : y z / y ≤ z }.
- -
-Lemma ler_wnmul2l x : x ≤ 0 → {homo *%R x : y z /~ y ≤ z }.
- -
-Lemma ler_wnmul2r x : x ≤ 0 → {homo *%R ^~ x : y z /~ y ≤ z }.
- -
-

- -

- Binary forms, for backchaining. -

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

- -

- complement for x *+ n and <= or < -

- -
-Lemma ler_pmuln2r n : (0 < n)%N → {mono (@GRing.natmul R )^~ n : x y / x ≤ y }.
- -
-Lemma ltr_pmuln2r n : (0 < n)%N → {mono (@GRing.natmul R )^~ n : x y / x < y }.
- -
-Lemma pmulrnI n : (0 < n)%N → injective ((@GRing.natmul R )^~ n).
- -
-Lemma eqr_pmuln2r n : (0 < n)%N → {mono (@GRing.natmul R )^~ n : x y / x == y }.
- -
-Lemma pmulrn_lgt0 x n : (0 < n)%N → (0 < x *+ n ) = (0 < x ).
- -
-Lemma pmulrn_llt0 x n : (0 < n)%N → (x *+ n < 0) = (x < 0).
- -
-Lemma pmulrn_lge0 x n : (0 < n)%N → (0 ≤ x *+ n ) = (0 ≤ x ).
- -
-Lemma pmulrn_lle0 x n : (0 < n)%N → (x *+ n ≤ 0) = (x ≤ 0).
- -
-Lemma ltr_wmuln2r x y n : x < y → (x *+ n < y *+ n ) = (0 < n)%N.
- -
-Lemma ltr_wpmuln2r n : (0 < n)%N → {homo (@GRing.natmul R )^~ n : x y / x < y }.
- -
-Lemma ler_wmuln2r n : {homo (@GRing.natmul R )^~ n : x y / x ≤ y }.
- -
-Lemma mulrn_wge0 x n : 0 ≤ x → 0 ≤ x *+ n.
- -
-Lemma mulrn_wle0 x n : x ≤ 0 → x *+ n ≤ 0.
- -
-Lemma ler_muln2r n x y : (x *+ n ≤ y *+ n ) = ((n == 0%N) || (x ≤ y )).
- -
-Lemma ltr_muln2r n x y : (x *+ n < y *+ n ) = ((0 < n)%N && (x < y )).
- -
-Lemma eqr_muln2r n x y : (x *+ n == y *+ n ) = (n == 0)%N || (x == y ).
- -
-

- -

- More characteristic zero properties. -

- -
-Lemma mulrn_eq0 x n : (x *+ n == 0) = ((n == 0)%N || (x == 0)).
- -
-Lemma mulrIn x : x != 0 → injective (GRing.natmul x).
- -
-Lemma ler_wpmuln2l x :
-  0 ≤ x → {homo (@GRing.natmul R x ) : m n / (m ≤ n)%N >-> m ≤ n }.
- -
-Lemma ler_wnmuln2l x :
-  x ≤ 0 → {homo (@GRing.natmul R x ) : m n / (n ≤ m)%N >-> m ≤ n }.
- -
-Lemma mulrn_wgt0 x n : 0 < x → 0 < x *+ n = (0 < n)%N.
- -
-Lemma mulrn_wlt0 x n : x < 0 → x *+ n < 0 = (0 < n)%N.
- -
-Lemma ler_pmuln2l x :
-  0 < x → {mono (@GRing.natmul R x ) : m n / (m ≤ n)%N >-> m ≤ n }.
- -
-Lemma ltr_pmuln2l x :
-  0 < x → {mono (@GRing.natmul R x ) : m n / (m < n)%N >-> m < n }.
- -
-Lemma ler_nmuln2l x :
-  x < 0 → {mono (@GRing.natmul R x ) : m n / (n ≤ m)%N >-> m ≤ n }.
- -
-Lemma ltr_nmuln2l x :
-  x < 0 → {mono (@GRing.natmul R x ) : m n / (n < m)%N >-> m < n }.
- -
-Lemma ler_nat m n : (m %:R ≤ n %:R :> R ) = (m ≤ n)%N.
- -
-Lemma ltr_nat m n : (m %:R < n %:R :> R ) = (m < n)%N.
- -
-Lemma eqr_nat m n : (m %:R == n %:R :> R ) = (m == n)%N.
- -
-Lemma pnatr_eq1 n : (n %:R == 1 :> R ) = (n == 1)%N.
- -
-Lemma lern0 n : (n %:R ≤ 0 :> R ) = (n == 0%N).
- -
-Lemma ltrn0 n : (n %:R < 0 :> R ) = false.
- -
-Lemma ler1n n : 1 ≤ n %:R :> R = (1 ≤ n)%N.
-Lemma ltr1n n : 1 < n %:R :> R = (1 < n)%N.
-Lemma lern1 n : n %:R ≤ 1 :> R = (n ≤ 1)%N.
-Lemma ltrn1 n : n %:R < 1 :> R = (n < 1)%N.
- -
-Lemma ltrN10 : -1 < 0 :> R.
-Lemma lerN10 : -1 ≤ 0 :> R.
-Lemma ltr10 : 1 < 0 :> R = false.
-Lemma ler10 : 1 ≤ 0 :> R = false.
-Lemma ltr0N1 : 0 < -1 :> R = false.
-Lemma ler0N1 : 0 ≤ -1 :> R = false.
- -
-Lemma pmulrn_rgt0 x n : 0 < x → 0 < x *+ n = (0 < n)%N.
- -
-Lemma pmulrn_rlt0 x n : 0 < x → x *+ n < 0 = false.
- -
-Lemma pmulrn_rge0 x n : 0 < x → 0 ≤ x *+ n.
- -
-Lemma pmulrn_rle0 x n : 0 < x → x *+ n ≤ 0 = (n == 0)%N.
- -
-Lemma nmulrn_rgt0 x n : x < 0 → 0 < x *+ n = false.
- -
-Lemma nmulrn_rge0 x n : x < 0 → 0 ≤ x *+ n = (n == 0)%N.
- -
-Lemma nmulrn_rle0 x n : x < 0 → x *+ n ≤ 0.
- -
-

- -

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

- - x positive and y right -

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

- -

- x positive and y left -

-Lemma pmulr_lgt0 x y : 0 < x → (0 < y × x ) = (0 < y ).
- -
-Lemma pmulr_lge0 x y : 0 < x → (0 ≤ y × x ) = (0 ≤ y ).
- -
-Lemma pmulr_llt0 x y : 0 < x → (y × x < 0) = (y < 0).
- -
-Lemma pmulr_lle0 x y : 0 < x → (y × x ≤ 0) = (y ≤ 0).
- -
-

- -

- x negative and y right -

-Lemma nmulr_rgt0 x y : x < 0 → (0 < x × y ) = (y < 0).
- -
-Lemma nmulr_rge0 x y : x < 0 → (0 ≤ x × y ) = (y ≤ 0).
- -
-Lemma nmulr_rlt0 x y : x < 0 → (x × y < 0) = (0 < y ).
- -
-Lemma nmulr_rle0 x y : x < 0 → (x × y ≤ 0) = (0 ≤ y ).
- -
-

- -

- x negative and y left -

-Lemma nmulr_lgt0 x y : x < 0 → (0 < y × x ) = (y < 0).
- -
-Lemma nmulr_lge0 x y : x < 0 → (0 ≤ y × x ) = (y ≤ 0).
- -
-Lemma nmulr_llt0 x y : x < 0 → (y × x < 0) = (0 < y ).
- -
-Lemma nmulr_lle0 x y : x < 0 → (y × x ≤ 0) = (0 ≤ y ).
- -
-

- -

- weak and symmetric lemmas -

-Lemma mulr_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x × y.
- -
-Lemma mulr_le0 x y : x ≤ 0 → y ≤ 0 → 0 ≤ x × y.
- -
-Lemma mulr_ge0_le0 x y : 0 ≤ x → y ≤ 0 → x × y ≤ 0.
- -
-Lemma mulr_le0_ge0 x y : x ≤ 0 → 0 ≤ y → x × y ≤ 0.
- -
-

- -

- mulr_gt0 with only one case -

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

- -

- Iterated products -

- -
-Lemma prodr_ge0 I r (P : pred I) (E : I → R) :
-  (∀ i, P i → 0 ≤ E i ) → 0 ≤ \prod_(i <- r | P i ) E i.
- -
-Lemma prodr_gt0 I r (P : pred I) (E : I → R) :
-  (∀ i, P i → 0 < E i ) → 0 < \prod_(i <- r | P i ) E i.
- -
-Lemma ler_prod I r (P : pred I) (E1 E2 : I → R) :
-    (∀ i, P i → 0 ≤ E1 i ≤ E2 i ) →
-  \prod_(i <- r | P i ) E1 i ≤ \prod_(i <- r | P i ) E2 i.
- -
-Lemma ltr_prod I r (P : pred I) (E1 E2 : I → R) :
-    has P r → (∀ i, P i → 0 ≤ E1 i < E2 i ) →
-  \prod_(i <- r | P i ) E1 i < \prod_(i <- r | P i ) E2 i.
- -
-Lemma ltr_prod_nat (E1 E2 : nat → R) (n m : nat) :
-   (m < n)%N → (∀ i, (m ≤ i < n)%N → 0 ≤ E1 i < E2 i ) →
-  \prod_(m ≤ i < n ) E1 i < \prod_(m ≤ i < n ) E2 i.
- -
-

- -

- real of mul -

- -
-Lemma realMr x y : x != 0 → x \is real → (x × y \is real ) = (y \is real ).
- -
-Lemma realrM x y : y != 0 → y \is real → (x × y \is real ) = (x \is real ).
- -
-Lemma realM : {in real &, ∀ x y, x × y \is real }.
- -
-Lemma realrMn x n : (n != 0)%N → (x *+ n \is real ) = (x \is real ).
- -
-

- -

- ler/ltr and multiplication between a positive/negative -

- -
-Lemma ger_pmull x y : 0 < y → (x × y ≤ y ) = (x ≤ 1).
- -
-Lemma gtr_pmull x y : 0 < y → (x × y < y ) = (x < 1).
- -
-Lemma ger_pmulr x y : 0 < y → (y × x ≤ y ) = (x ≤ 1).
- -
-Lemma gtr_pmulr x y : 0 < y → (y × x < y ) = (x < 1).
- -
-Lemma ler_pmull x y : 0 < y → (y ≤ x × y ) = (1 ≤ x ).
- -
-Lemma ltr_pmull x y : 0 < y → (y < x × y ) = (1 < x ).
- -
-Lemma ler_pmulr x y : 0 < y → (y ≤ y × x ) = (1 ≤ x ).
- -
-Lemma ltr_pmulr x y : 0 < y → (y < y × x ) = (1 < x ).
- -
-Lemma ger_nmull x y : y < 0 → (x × y ≤ y ) = (1 ≤ x ).
- -
-Lemma gtr_nmull x y : y < 0 → (x × y < y ) = (1 < x ).
- -
-Lemma ger_nmulr x y : y < 0 → (y × x ≤ y ) = (1 ≤ x ).
- -
-Lemma gtr_nmulr x y : y < 0 → (y × x < y ) = (1 < x ).
- -
-Lemma ler_nmull x y : y < 0 → (y ≤ x × y ) = (x ≤ 1).
- -
-Lemma ltr_nmull x y : y < 0 → (y < x × y ) = (x < 1).
- -
-Lemma ler_nmulr x y : y < 0 → (y ≤ y × x ) = (x ≤ 1).
- -
-Lemma ltr_nmulr x y : y < 0 → (y < y × x ) = (x < 1).
- -
-

- -

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

- -
-Lemma ler_pemull x y : 0 ≤ y → 1 ≤ x → y ≤ x × y.
- -
-Lemma ler_nemull x y : y ≤ 0 → 1 ≤ x → x × y ≤ y.
- -
-Lemma ler_pemulr x y : 0 ≤ y → 1 ≤ x → y ≤ y × x.
- -
-Lemma ler_nemulr x y : y ≤ 0 → 1 ≤ x → y × x ≤ y.
- -
-Lemma ler_pimull x y : 0 ≤ y → x ≤ 1 → x × y ≤ y.
- -
-Lemma ler_nimull x y : y ≤ 0 → x ≤ 1 → y ≤ x × y.
- -
-Lemma ler_pimulr x y : 0 ≤ y → x ≤ 1 → y × x ≤ y.
- -
-Lemma ler_nimulr x y : y ≤ 0 → x ≤ 1 → y ≤ y × x.
- -
-Lemma mulr_ile1 x y : 0 ≤ x → 0 ≤ y → x ≤ 1 → y ≤ 1 → x × y ≤ 1.
- -
-Lemma mulr_ilt1 x y : 0 ≤ x → 0 ≤ y → x < 1 → y < 1 → x × y < 1.
- -
-Definition mulr_ilte1 := (mulr_ile1 , mulr_ilt1 ).
- -
-Lemma mulr_ege1 x y : 1 ≤ x → 1 ≤ y → 1 ≤ x × y.
- -
-Lemma mulr_egt1 x y : 1 < x → 1 < y → 1 < x × y.
-Definition mulr_egte1 := (mulr_ege1 , mulr_egt1 ).
-Definition mulr_cp1 := (mulr_ilte1 , mulr_egte1 ).
- -
-

- -

- ler and ^-1 -

- -
-Lemma invr_gt0 x : (0 < x ^-1 ) = (0 < x ).
- -
-Lemma invr_ge0 x : (0 ≤ x ^-1 ) = (0 ≤ x ).
- -
-Lemma invr_lt0 x : (x ^-1 < 0) = (x < 0).
- -
-Lemma invr_le0 x : (x ^-1 ≤ 0) = (x ≤ 0).
- -
-Definition invr_gte0 := (invr_ge0 , invr_gt0 ).
-Definition invr_lte0 := (invr_le0 , invr_lt0 ).
- -
-Lemma divr_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x / y.
- -
-Lemma divr_gt0 x y : 0 < x → 0 < y → 0 < x / y.
- -
-Lemma realV : {mono (@GRing.inv R ) : x / x \is real }.
- -
-

- -

- ler and exprn -

-Lemma exprn_ge0 n x : 0 ≤ x → 0 ≤ x ^+ n.
- -
-Lemma realX n : {in real , ∀ x, x ^+ n \is real }.
- -
-Lemma exprn_gt0 n x : 0 < x → 0 < x ^+ n.
- -
-Definition exprn_gte0 := (exprn_ge0 , exprn_gt0 ).
- -
-Lemma exprn_ile1 n x : 0 ≤ x → x ≤ 1 → x ^+ n ≤ 1.
- -
-Lemma exprn_ilt1 n x : 0 ≤ x → x < 1 → x ^+ n < 1 = (n != 0%N).
- -
-Definition exprn_ilte1 := (exprn_ile1 , exprn_ilt1 ).
- -
-Lemma exprn_ege1 n x : 1 ≤ x → 1 ≤ x ^+ n.
- -
-Lemma exprn_egt1 n x : 1 < x → 1 < x ^+ n = (n != 0%N).
- -
-Definition exprn_egte1 := (exprn_ege1 , exprn_egt1 ).
-Definition exprn_cp1 := (exprn_ilte1 , exprn_egte1 ).
- -
-Lemma ler_iexpr x n : (0 < n)%N → 0 ≤ x → x ≤ 1 → x ^+ n ≤ x.
- -
-Lemma ltr_iexpr x n : 0 < x → x < 1 → (x ^+ n < x ) = (1 < n)%N.
- -
-Definition lter_iexpr := (ler_iexpr , ltr_iexpr ).
- -
-Lemma ler_eexpr x n : (0 < n)%N → 1 ≤ x → x ≤ x ^+ n.
- -
-Lemma ltr_eexpr x n : 1 < x → (x < x ^+ n ) = (1 < n)%N.
- -
-Definition lter_eexpr := (ler_eexpr , ltr_eexpr ).
-Definition lter_expr := (lter_iexpr , lter_eexpr ).
- -
-Lemma ler_wiexpn2l x :
-  0 ≤ x → x ≤ 1 → {homo (GRing.exp x ) : m n / (n ≤ m)%N >-> m ≤ n }.
- -
-Lemma ler_weexpn2l x :
-  1 ≤ x → {homo (GRing.exp x ) : m n / (m ≤ n)%N >-> m ≤ n }.
- -
-Lemma ieexprn_weq1 x n : 0 ≤ x → (x ^+ n == 1) = ((n == 0%N) || (x == 1)).
- -
-Lemma ieexprIn x : 0 < x → x != 1 → injective (GRing.exp x).
- -
-Lemma ler_iexpn2l x :
-  0 < x → x < 1 → {mono (GRing.exp x ) : m n / (n ≤ m)%N >-> m ≤ n }.
- -
-Lemma ltr_iexpn2l x :
-  0 < x → x < 1 → {mono (GRing.exp x ) : m n / (n < m)%N >-> m < n }.
- -
-Definition lter_iexpn2l := (ler_iexpn2l , ltr_iexpn2l ).
- -
-Lemma ler_eexpn2l x :
-  1 < x → {mono (GRing.exp x ) : m n / (m ≤ n)%N >-> m ≤ n }.
- -
-Lemma ltr_eexpn2l x :
-  1 < x → {mono (GRing.exp x ) : m n / (m < n)%N >-> m < n }.
- -
-Definition lter_eexpn2l := (ler_eexpn2l , ltr_eexpn2l ).
- -
-Lemma ltr_expn2r n x y : 0 ≤ x → x < y → x ^+ n < y ^+ n = (n != 0%N).
- -
-Lemma ler_expn2r n : {in nneg & , {homo ((@GRing.exp R )^~ n ) : x y / x ≤ y }}.
- -
-Definition lter_expn2r := (ler_expn2r , ltr_expn2r ).
- -
-Lemma ltr_wpexpn2r n :
-  (0 < n)%N → {in nneg & , {homo ((@GRing.exp R )^~ n ) : x y / x < y }}.
- -
-Lemma ler_pexpn2r n :
-  (0 < n)%N → {in nneg & , {mono ((@GRing.exp R )^~ n ) : x y / x ≤ y }}.
- -
-Lemma ltr_pexpn2r n :
-  (0 < n)%N → {in nneg & , {mono ((@GRing.exp R )^~ n ) : x y / x < y }}.
- -
-Definition lter_pexpn2r := (ler_pexpn2r , ltr_pexpn2r ).
- -
-Lemma pexpIrn n : (0 < n)%N → {in nneg &, injective ((@GRing.exp R )^~ n)}.
- -
-

- -

- expr and ler/ltr -

-Lemma expr_le1 n x : (0 < n)%N → 0 ≤ x → (x ^+ n ≤ 1) = (x ≤ 1).
- -
-Lemma expr_lt1 n x : (0 < n)%N → 0 ≤ x → (x ^+ n < 1) = (x < 1).
- -
-Definition expr_lte1 := (expr_le1 , expr_lt1 ).
- -
-Lemma expr_ge1 n x : (0 < n)%N → 0 ≤ x → (1 ≤ x ^+ n ) = (1 ≤ x ).
- -
-Lemma expr_gt1 n x : (0 < n)%N → 0 ≤ x → (1 < x ^+ n ) = (1 < x ).
- -
-Definition expr_gte1 := (expr_ge1 , expr_gt1 ).
- -
-Lemma pexpr_eq1 x n : (0 < n)%N → 0 ≤ x → (x ^+ n == 1) = (x == 1).
- -
-Lemma pexprn_eq1 x n : 0 ≤ x → (x ^+ n == 1) = (n == 0%N) || (x == 1).
- -
-Lemma eqr_expn2 n x y :
-  (0 < n)%N → 0 ≤ x → 0 ≤ y → (x ^+ n == y ^+ n ) = (x == y ).
- -
-Lemma sqrp_eq1 x : 0 ≤ x → (x ^+ 2 == 1) = (x == 1).
- -
-Lemma sqrn_eq1 x : x ≤ 0 → (x ^+ 2 == 1) = (x == -1).
- -
-Lemma ler_sqr : {in nneg &, {mono (fun x ⇒ x ^+ 2) : x y / x ≤ y }}.
- -
-Lemma ltr_sqr : {in nneg &, {mono (fun x ⇒ x ^+ 2) : x y / x < y }}.
- -
-Lemma ler_pinv :
-  {in [pred x in GRing.unit | 0 < x ] &, {mono (@GRing.inv R ) : x y /~ x ≤ y }}.
- -
-Lemma ler_ninv :
-  {in [pred x in GRing.unit | x < 0] &, {mono (@GRing.inv R ) : x y /~ x ≤ y }}.
- -
-Lemma ltr_pinv :
-  {in [pred x in GRing.unit | 0 < x ] &, {mono (@GRing.inv R ) : x y /~ x < y }}.
- -
-Lemma ltr_ninv :
-  {in [pred x in GRing.unit | x < 0] &, {mono (@GRing.inv R ) : x y /~ x < y }}.
- -
-Lemma invr_gt1 x : x \is a GRing.unit → 0 < x → (1 < x ^-1 ) = (x < 1).
- -
-Lemma invr_ge1 x : x \is a GRing.unit → 0 < x → (1 ≤ x ^-1 ) = (x ≤ 1).
- -
-Definition invr_gte1 := (invr_ge1 , invr_gt1 ).
- -
-Lemma invr_le1 x (ux : x \is a GRing.unit) (hx : 0 < x) :
-  (x ^-1 ≤ 1) = (1 ≤ x ).
- -
-Lemma invr_lt1 x (ux : x \is a GRing.unit) (hx : 0 < x) : (x ^-1 < 1) = (1 < x ).
- -
-Definition invr_lte1 := (invr_le1 , invr_lt1 ).
-Definition invr_cp1 := (invr_gte1 , invr_lte1 ).
- -
-

- -

- norm -

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

- -

- norm + add -

- -

- GG: Could this be a better definition of "real" ? -

-Lemma realEsqr x : (x \is real ) = (0 ≤ x ^+ 2).
- -
-Lemma real_normK x : x \is real → `|x | ^+ 2 = x ^+ 2.
- -
-

- -

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

- -
-Lemma normr_sign s : `|(-1) ^+ s | = 1 :> R.
- -
-Lemma normrMsign s x : `|(-1) ^+ s × x | = `|x |.
- -
-Lemma signr_gt0 (b : bool) : (0 < (-1) ^+ b :> R ) = ~~ b.
- -
-Lemma signr_lt0 (b : bool) : ((-1) ^+ b < 0 :> R ) = b.
- -
-Lemma signr_ge0 (b : bool) : (0 ≤ (-1) ^+ b :> R ) = ~~ b.
- -
-Lemma signr_le0 (b : bool) : ((-1) ^+ b ≤ 0 :> R ) = b.
- -
-

- -

- This actually holds for char R != 2. -

-Lemma signr_inj : injective (fun b : bool ⇒ (-1) ^+ b : R).
- -
-

- -

- Ternary sign (sg). -

- -
-Lemma sgr_def x : sg x = (-1) ^+ (x < 0)%R *+ (x != 0).
- -
-Lemma neqr0_sign x : x != 0 → (-1) ^+ (x < 0)%R = sgr x.
- -
-Lemma gtr0_sg x : 0 < x → sg x = 1.
- -
-Lemma ltr0_sg x : x < 0 → sg x = -1.
- -
-Lemma sgr0 : sg 0 = 0 :> R.
-Lemma sgr1 : sg 1 = 1 :> R.
-Lemma sgrN1 : sg (-1) = -1 :> R.
-Definition sgrE := (sgr0 , sgr1 , sgrN1 ).
- -
-Lemma sqr_sg x : sg x ^+ 2 = (x != 0)%:R.
- -
-Lemma mulr_sg_eq1 x y : (sg x × y == 1) = (x != 0) && (sg x == y ).
- -
-Lemma mulr_sg_eqN1 x y : (sg x × sg y == -1) = (x != 0) && (sg x == - sg y ).
- -
-Lemma sgr_eq0 x : (sg x == 0) = (x == 0).
- -
-Lemma sgr_odd n x : x != 0 → (sg x ) ^+ n = (sg x ) ^+ (odd n ).
- -
-Lemma sgrMn x n : sg (x *+ n) = (n != 0%N)%:R × sg x.
- -
-Lemma sgr_nat n : sg n %:R = (n != 0%N)%:R :> R.
- -
-Lemma sgr_id x : sg (sg x) = sg x.
- -
-Lemma sgr_lt0 x : (sg x < 0) = (x < 0).
- -
-Lemma sgr_le0 x : (sgr x ≤ 0) = (x ≤ 0).
- -
-

- -

- sign and norm -

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

- -

- GG: pointless duplication... -

-Lemma real_mulr_sign_norm x : x \is real → (-1) ^+ (x < 0)%R × `|x | = x.
- -
-Lemma real_mulr_Nsign_norm x : x \is real → (-1) ^+ (0 < x)%R × `|x | = - x.
- -
-Lemma realEsg x : x \is real → x = sgr x × `|x |.
- -
-Lemma normr_sg x : `|sg x | = (x != 0)%:R.
- -
-Lemma sgr_norm x : sg `|x | = (x != 0)%:R.
- -
-

- -

- lerif -

- -
-Lemma lerif_refl x C : reflect (x ≤ x ?= iff C) C.
- -
-Lemma lerif_trans x1 x2 x3 C12 C23 :
-  x1 ≤ x2 ?= iff C12 → x2 ≤ x3 ?= iff C23 → x1 ≤ x3 ?= iff C12 && C23.
- -
-Lemma lerif_le x y : x ≤ y → x ≤ y ?= iff (x ≥ y ).
- -
-Lemma lerif_eq x y : x ≤ y → x ≤ y ?= iff (x == y ).
- -
-Lemma ger_lerif x y C : x ≤ y ?= iff C → (y ≤ x ) = C.
- -
-Lemma ltr_lerif x y C : x ≤ y ?= iff C → (x < y ) = ~~ C.
- -
-Lemma lerif_nat m n C : (m %:R ≤ n %:R ?= iff C :> R ) = (m ≤ n ?= iff C)%N.
- -
-Lemma mono_in_lerif (A : {pred R }) (f : R → R) C :
-   {in A &, {mono f : x y / x ≤ y }} →
-  {in A &, ∀ x y, (f x ≤ f y ?= iff C ) = (x ≤ y ?= iff C )}.
- -
-Lemma mono_lerif (f : R → R) C :
-    {mono f : x y / x ≤ y } →
-  ∀ x y, (f x ≤ f y ?= iff C ) = (x ≤ y ?= iff C ).
- -
-Lemma nmono_in_lerif (A : {pred R }) (f : R → R) C :
-    {in A &, {mono f : x y /~ x ≤ y }} →
-  {in A &, ∀ x y, (f x ≤ f y ?= iff C ) = (y ≤ x ?= iff C )}.
- -
-Lemma nmono_lerif (f : R → R) C :
-    {mono f : x y /~ x ≤ y } →
-  ∀ x y, (f x ≤ f y ?= iff C ) = (y ≤ x ?= iff C ).
- -
-Lemma lerif_subLR x y z C : (x - y ≤ z ?= iff C ) = (x ≤ z + y ?= iff C ).
- -
-Lemma lerif_subRL x y z C : (x ≤ y - z ?= iff C ) = (x + z ≤ y ?= iff C ).
- -
-Lemma lerif_add x1 y1 C1 x2 y2 C2 :
-    x1 ≤ y1 ?= iff C1 → x2 ≤ y2 ?= iff C2 →
-  x1 + x2 ≤ y1 + y2 ?= iff C1 && C2.
- -
-Lemma lerif_sum (I : finType) (P C : pred I) (E1 E2 : I → R) :
-    (∀ i, P i → E1 i ≤ E2 i ?= iff C i ) →
-  \sum_(i | P i ) E1 i ≤ \sum_(i | P i ) E2 i ?= iff [∀ (i | P i ), C i ].
- -
-Lemma lerif_0_sum (I : finType) (P C : pred I) (E : I → R) :
-    (∀ i, P i → 0 ≤ E i ?= iff C i ) →
-  0 ≤ \sum_(i | P i ) E i ?= iff [∀ (i | P i ), C i ].
- -
-Lemma real_lerif_norm x : x \is real → x ≤ `|x | ?= iff (0 ≤ x ).
- -
-Lemma lerif_pmul x1 x2 y1 y2 C1 C2 :
-    0 ≤ x1 → 0 ≤ x2 → x1 ≤ y1 ?= iff C1 → x2 ≤ y2 ?= iff C2 →
-  x1 × x2 ≤ y1 × y2 ?= iff (y1 × y2 == 0) || C1 && C2.
- -
-Lemma lerif_nmul x1 x2 y1 y2 C1 C2 :
-    y1 ≤ 0 → y2 ≤ 0 → x1 ≤ y1 ?= iff C1 → x2 ≤ y2 ?= iff C2 →
-  y1 × y2 ≤ x1 × x2 ?= iff (x1 × x2 == 0) || C1 && C2.
- -
-Lemma lerif_pprod (I : finType) (P C : pred I) (E1 E2 : I → R) :
-    (∀ i, P i → 0 ≤ E1 i ) →
-    (∀ i, P i → E1 i ≤ E2 i ?= iff C i ) →
-  let pi E := \prod_(i | P i ) E i in
-  pi E1 ≤ pi E2 ?= iff (pi E2 == 0) || [∀ (i | P i ), C i ].
- -
-

- -

- Mean inequalities. -

- -
-Lemma real_lerif_mean_square_scaled x y :
-  x \is real → y \is real → x × y *+ 2 ≤ x ^+ 2 + y ^+ 2 ?= iff (x == y ).
- -
-Lemma real_lerif_AGM2_scaled x y :
-  x \is real → y \is real → x × y *+ 4 ≤ (x + y ) ^+ 2 ?= iff (x == y ).
- -
-Lemma lerif_AGM_scaled (I : finType) (A : {pred I }) (E : I → R) (n := #|A |) :
-    {in A , ∀ i, 0 ≤ E i *+ n } →
-  \prod_(i in A ) (E i *+ n ) ≤ (\sum_(i in A ) E i ) ^+ n
-                            ?= iff [∀ i in A , ∀ j in A , E i == E j ].
- -
-

- -

- Polynomial bound. -

- -
-Implicit Type p : {poly R }.
- -
-Lemma poly_disk_bound p b : {ub | ∀ x, `|x | ≤ b → `|p .[x ]| ≤ ub }.
- -
-End NumDomainOperationTheory.
- -
-Hint Resolve ler_opp2 ltr_opp2 real0 real1 normr_real : core.
- -
-Section NumDomainMonotonyTheoryForReals.
- -
-Variables (R R' : numDomainType) (D : pred R) (f : R → R') (f' : R → nat).
-Implicit Types (m n p : nat) (x y z : R) (u v w : R').
- -
-Lemma real_mono :
-  {homo f : x y / x < y } → {in real &, {mono f : x y / x ≤ y }}.
- -
-Lemma real_nmono :
-  {homo f : x y /~ x < y } → {in real &, {mono f : x y /~ x ≤ y }}.
- -
-Lemma real_mono_in :
-    {in D &, {homo f : x y / x < y }} →
-  {in [pred x in D | x \is real ] &, {mono f : x y / x ≤ y }}.
- -
-Lemma real_nmono_in :
-    {in D &, {homo f : x y /~ x < y }} →
-  {in [pred x in D | x \is real ] &, {mono f : x y /~ x ≤ y }}.
- -
-Lemma realn_mono : {homo f' : x y / x < y >-> (x < y)%N} →
-  {in real &, {mono f' : x y / x ≤ y >-> (x ≤ y)%N}}.
- -
-Lemma realn_nmono : {homo f' : x y / y < x >-> (x < y)%N} →
-  {in real &, {mono f' : x y / y ≤ x >-> (x ≤ y)%N}}.
- -
-Lemma realn_mono_in : {in D &, {homo f' : x y / x < y >-> (x < y)%N}} →
-  {in [pred x in D | x \is real ] &, {mono f' : x y / x ≤ y >-> (x ≤ y)%N}}.
- -
-Lemma realn_nmono_in : {in D &, {homo f' : x y / y < x >-> (x < y)%N}} →
-  {in [pred x in D | x \is real ] &, {mono f' : x y / y ≤ x >-> (x ≤ y)%N}}.
- -
-End NumDomainMonotonyTheoryForReals.
- -
-Section FinGroup.
- -
-Import GroupScope.
- -
-Variables (R : numDomainType) (gT : finGroupType).
-Implicit Types G : {group gT }.
- -
-Lemma natrG_gt0 G : #|G |%:R > 0 :> R.
- -
-Lemma natrG_neq0 G : #|G |%:R != 0 :> R.
- -
-Lemma natr_indexg_gt0 G B : #|G : B |%:R > 0 :> R.
- -
-Lemma natr_indexg_neq0 G B : #|G : B |%:R != 0 :> R.
- -
-End FinGroup.
- -
-Section NumFieldTheory.
- -
-Variable F : numFieldType.
-Implicit Types x y z t : F.
- -
-Lemma unitf_gt0 x : 0 < x → x \is a GRing.unit.
- -
-Lemma unitf_lt0 x : x < 0 → x \is a GRing.unit.
- -
-Lemma lef_pinv : {in pos &, {mono (@GRing.inv F ) : x y /~ x ≤ y }}.
- -
-Lemma lef_ninv : {in neg &, {mono (@GRing.inv F ) : x y /~ x ≤ y }}.
- -
-Lemma ltf_pinv : {in pos &, {mono (@GRing.inv F ) : x y /~ x < y }}.
- -
-Lemma ltf_ninv: {in neg &, {mono (@GRing.inv F ) : x y /~ x < y }}.
- -
-Definition ltef_pinv := (lef_pinv , ltf_pinv ).
-Definition ltef_ninv := (lef_ninv , ltf_ninv ).
- -
-Lemma invf_gt1 x : 0 < x → (1 < x ^-1 ) = (x < 1).
- -
-Lemma invf_ge1 x : 0 < x → (1 ≤ x ^-1 ) = (x ≤ 1).
- -
-Definition invf_gte1 := (invf_ge1 , invf_gt1 ).
- -
-Lemma invf_le1 x : 0 < x → (x ^-1 ≤ 1) = (1 ≤ x ).
- -
-Lemma invf_lt1 x : 0 < x → (x ^-1 < 1) = (1 < x ).
- -
-Definition invf_lte1 := (invf_le1 , invf_lt1 ).
-Definition invf_cp1 := (invf_gte1 , invf_lte1 ).
- -
-

- -

- These lemma are all combinations of mono(LR|RL) with ler [pn]mul2[rl]. -

- -

- Interval midpoint. -

- -
- -
-Lemma midf_le x y : x ≤ y → (x ≤ mid x y ) × (mid x y ≤ y ).
- -
-Lemma midf_lt x y : x < y → (x < mid x y ) × (mid x y < y ).
- -
-Definition midf_lte := (midf_le , midf_lt ).
- -
-

- -

- The AGM, unscaled but without the nth root. -

- -
-Lemma real_lerif_mean_square x y :
-  x \is real → y \is real → x × y ≤ mid (x ^+ 2) (y ^+ 2) ?= iff (x == y ).
- -
-Lemma real_lerif_AGM2 x y :
-  x \is real → y \is real → x × y ≤ mid x y ^+ 2 ?= iff (x == y ).
- -
-Lemma lerif_AGM (I : finType) (A : {pred I }) (E : I → F) :
-    let n := #|A | in let mu := (\sum_(i in A ) E i ) / n %:R in
-    {in A , ∀ i, 0 ≤ E i } →
-  \prod_(i in A ) E i ≤ mu ^+ n
-                     ?= iff [∀ i in A , ∀ j in A , E i == E j ].
- -
-Implicit Type p : {poly F }.
-Lemma Cauchy_root_bound p : p != 0 → {b | ∀ x, root p x → `|x | ≤ b }.
- -
-Import GroupScope.
- -
-Lemma natf_indexg (gT : finGroupType) (G H : {group gT }) :
-  H \subset G → #|G : H |%:R = (#|G |%:R / #|H |%:R)%R :> F.
- -
-End NumFieldTheory.
- -
-Section RealDomainTheory.
- -
-Hint Resolve lerr : core.
- -
-Variable R : realDomainType.
-Implicit Types x y z t : R.
- -
-Lemma num_real x : x \is real.
-Hint Resolve num_real : core.
- -
-Lemma ler_total : total (@le R).
- -
-Lemma ltr_total x y : x != y → (x < y ) || (y < x ).
- -
-Lemma wlog_ler P :
-     (∀ a b, P b a → P a b ) → (∀ a b, a ≤ b → P a b ) →
-   ∀ a b : R, P a b.
- -
-Lemma wlog_ltr P :
-    (∀ a, P a a ) →
-    (∀ a b, (P b a → P a b)) → (∀ a b, a < b → P a b ) →
-  ∀ a b : R, P a b.
- -
-Lemma ltrNge x y : (x < y ) = ~~ (y ≤ x ).
- -
-Lemma lerNgt x y : (x ≤ y ) = ~~ (y < x ).
- -
-Lemma lerP x y : ler_xor_gt x y `|x - y | `|y - x | (x ≤ y) (y < x).
- -
-Lemma ltrP x y : ltr_xor_ge x y `|x - y | `|y - x | (y ≤ x) (x < y).
- -
-Lemma ltrgtP x y :
-   comparer x y `|x - y | `|y - x | (y == x) (x == y)
-                 (x ≤ y) (y ≤ x) (x < y) (x > y) .
- -
-Lemma ger0P x : ger0_xor_lt0 x `|x | (x < 0) (0 ≤ x).
- -
-Lemma ler0P x : ler0_xor_gt0 x `|x | (0 < x) (x ≤ 0).
- -
-Lemma ltrgt0P x :
-  comparer0 x `|x | (0 == x) (x == 0) (x ≤ 0) (0 ≤ x) (x < 0) (x > 0).
- -
-Lemma neqr_lt x y : (x != y ) = (x < y ) || (y < x ).
- -
-Lemma eqr_leLR x y z t :
-  (x ≤ y → z ≤ t ) → (y < x → t < z ) → (x ≤ y ) = (z ≤ t ).
- -
-Lemma eqr_leRL x y z t :
-  (x ≤ y → z ≤ t ) → (y < x → t < z ) → (z ≤ t ) = (x ≤ y ).
- -
-Lemma eqr_ltLR x y z t :
-  (x < y → z < t ) → (y ≤ x → t ≤ z ) → (x < y ) = (z < t ).
- -
-Lemma eqr_ltRL x y z t :
-  (x < y → z < t ) → (y ≤ x → t ≤ z ) → (z < t ) = (x < y ).
- -
-

- -

- sign -

- -
-Lemma mulr_lt0 x y :
-  (x × y < 0) = [&& x != 0, y != 0 & (x < 0) (+) (y < 0)].
- -
-Lemma neq0_mulr_lt0 x y :
-  x != 0 → y != 0 → (x × y < 0) = (x < 0) (+) (y < 0).
- -
-Lemma mulr_sign_lt0 (b : bool) x :
-  ((-1) ^+ b × x < 0) = (x != 0) && (b (+) (x < 0)%R).
- -
-

- -

- sign & norm -

- -
-Lemma mulr_sign_norm x : (-1) ^+ (x < 0)%R × `|x | = x.
- -
-Lemma mulr_Nsign_norm x : (-1) ^+ (0 < x)%R × `|x | = - x.
- -
-Lemma numEsign x : x = (-1) ^+ (x < 0)%R × `|x |.
- -
-Lemma numNEsign x : -x = (-1) ^+ (0 < x)%R × `|x |.
- -
-Lemma normrEsign x : `|x | = (-1) ^+ (x < 0)%R × x.
- -
-End RealDomainTheory.
- -
-Hint Resolve num_real : core.
- -
-Section RealDomainMonotony.
- -
-Variables (R : realDomainType) (R' : numDomainType) (D : pred R).
-Variables (f : R → R') (f' : R → nat).
-Implicit Types (m n p : nat) (x y z : R) (u v w : R').
- -
-Hint Resolve (@num_real R) : core.
- -
-Lemma ler_mono : {homo f : x y / x < y } → {mono f : x y / x ≤ y }.
- -
-Lemma ler_nmono : {homo f : x y /~ x < y } → {mono f : x y /~ x ≤ y }.
- -
-Lemma ler_mono_in :
-  {in D &, {homo f : x y / x < y }} → {in D &, {mono f : x y / x ≤ y }}.
- -
-Lemma ler_nmono_in :
-  {in D &, {homo f : x y /~ x < y }} → {in D &, {mono f : x y /~ x ≤ y }}.
- -
-Lemma lern_mono : {homo f' : m n / m < n >-> (m < n)%N} →
-   {mono f' : m n / m ≤ n >-> (m ≤ n)%N}.
- -
-Lemma lern_nmono : {homo f' : m n / n < m >-> (m < n)%N} →
-  {mono f' : m n / n ≤ m >-> (m ≤ n)%N}.
- -
-Lemma lern_mono_in : {in D &, {homo f' : m n / m < n >-> (m < n)%N}} →
-   {in D &, {mono f' : m n / m ≤ n >-> (m ≤ n)%N}}.
- -
-Lemma lern_nmono_in : {in D &, {homo f' : m n / n < m >-> (m < n)%N}} →
-  {in D &, {mono f' : m n / n ≤ m >-> (m ≤ n)%N}}.
- -
-End RealDomainMonotony.
- -
-Section RealDomainArgExtremum.
- -
-Context {R : realDomainType} {I : finType} (i0 : I).
-Context (P : pred I) (F : I → R) (Pi0 : P i0).
- -
-Definition arg_minr := extremum <=%R i0 P F.
-Definition arg_maxr := extremum >=%R i0 P F.
- -
-Lemma arg_minrP: extremum_spec <=%R P F arg_minr.
- -
-Lemma arg_maxrP: extremum_spec >=%R P F arg_maxr.
- -
-End RealDomainArgExtremum.
- -
-Notation "[ 'arg' 'minr_' ( i < i0 | P ) F ]" :=
-    (arg_minr i0 (fun i ⇒ P%B) (fun i ⇒ F))
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg' 'minr_' ( i < i0 | P ) F ]") : form_scope.
- -
-Notation "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]" :=
-    [arg minr_(i < i0 | i \in A) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]") : form_scope.
- -
-Notation "[ 'arg' 'minr_' ( i < i0 ) F ]" := [arg minr_(i < i0 | true ) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg' 'minr_' ( i < i0 ) F ]") : form_scope.
- -
-Notation "[ 'arg' 'maxr_' ( i > i0 | P ) F ]" :=
-     (arg_maxr i0 (fun i ⇒ P%B) (fun i ⇒ F))
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg' 'maxr_' ( i > i0 | P ) F ]") : form_scope.
- -
-Notation "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]" :=
-    [arg maxr_(i > i0 | i \in A) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]") : form_scope.
- -
-Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true ) F]
-  (at level 0, i, i0 at level 10,
-   format "[ 'arg' 'maxr_' ( i > i0 ) F ]") : form_scope.
- -
-Section RealDomainOperations.
- -
-

- -

- sgr section -

- -
-Variable R : realDomainType.
-Implicit Types x y z t : R.
-Hint Resolve (@num_real R) : core.
- -
-Lemma sgr_cp0 x :
-  ((sg x == 1) = (0 < x )) ×
-  ((sg x == -1) = (x < 0)) ×
-  ((sg x == 0) = (x == 0)).
- -
-Variant sgr_val x : R → bool → bool → bool → bool → bool → bool
-  → bool → bool → bool → bool → bool → bool → R → Set :=
-  | SgrNull of x = 0 : sgr_val x 0 true true true true false false
-    true false false true false false 0
-  | SgrPos of x > 0 : sgr_val x x false false true false false true
-    false false true false false true 1
-  | SgrNeg of x < 0 : sgr_val x (- x) false true false false true false
-    false true false false true false (-1).
- -
-Lemma sgrP x :
-  sgr_val x `|x | (0 == x) (x ≤ 0) (0 ≤ x) (x == 0) (x < 0) (0 < x)
-                 (0 == sg x) (-1 == sg x) (1 == sg x)
-                 (sg x == 0) (sg x == -1) (sg x == 1) (sg x).
- -
-Lemma normrEsg x : `|x | = sg x × x.
- -
-Lemma numEsg x : x = sg x × `|x |.
- -
-

- -

- GG: duplicate! -

-Lemma mulr_sg_norm x : sg x × `|x | = x.
- -
-Lemma sgrM x y : sg (x × y) = sg x × sg y.
- -
-Lemma sgrN x : sg (- x) = - sg x.
- -
-Lemma sgrX n x : sg (x ^+ n) = (sg x ) ^+ n.
- -
-Lemma sgr_smul x y : sg (sg x × y) = sg x × sg y.
- -
-Lemma sgr_gt0 x : (sg x > 0) = (x > 0).
- -
-Lemma sgr_ge0 x : (sgr x ≥ 0) = (x ≥ 0).
- -
-

- -

- norm section -

- -
-Lemma ler_norm x : (x ≤ `|x |).
- -
-Lemma ler_norml x y : (`|x | ≤ y ) = (- y ≤ x ≤ y ).
- -
-Lemma ler_normlP x y : reflect ((- x ≤ y ) × (x ≤ y )) (`|x | ≤ y).
- -
-Lemma eqr_norml x y : (`|x | == y ) = ((x == y ) || (x == -y )) && (0 ≤ y ).
- -
-Lemma eqr_norm2 x y : (`|x | == `|y |) = (x == y ) || (x == -y ).
- -
-Lemma ltr_norml x y : (`|x | < y ) = (- y < x < y ).
- -
-Definition lter_norml := (ler_norml , ltr_norml ).
- -
-Lemma ltr_normlP x y : reflect ((-x < y ) × (x < y )) (`|x | < y).
- -
-Lemma ler_normr x y : (x ≤ `|y |) = (x ≤ y ) || (x ≤ - y ).
- -
-Lemma ltr_normr x y : (x < `|y |) = (x < y ) || (x < - y ).
- -
-Definition lter_normr := (ler_normr , ltr_normr ).
- -
-Lemma ler_distl x y e : (`|x - y | ≤ e ) = (y - e ≤ x ≤ y + e ).
- -
-Lemma ltr_distl x y e : (`|x - y | < e ) = (y - e < x < y + e ).
- -
-Definition lter_distl := (ler_distl , ltr_distl ).
- -
-Lemma exprn_even_ge0 n x : ~~ odd n → 0 ≤ x ^+ n.
- -
-Lemma exprn_even_gt0 n x : ~~ odd n → (0 < x ^+ n ) = (n == 0)%N || (x != 0).
- -
-Lemma exprn_even_le0 n x : ~~ odd n → (x ^+ n ≤ 0) = (n != 0%N) && (x == 0).
- -
-Lemma exprn_even_lt0 n x : ~~ odd n → (x ^+ n < 0) = false.
- -
-Lemma exprn_odd_ge0 n x : odd n → (0 ≤ x ^+ n ) = (0 ≤ x ).
- -
-Lemma exprn_odd_gt0 n x : odd n → (0 < x ^+ n ) = (0 < x ).
- -
-Lemma exprn_odd_le0 n x : odd n → (x ^+ n ≤ 0) = (x ≤ 0).
- -
-Lemma exprn_odd_lt0 n x : odd n → (x ^+ n < 0) = (x < 0).
- -
-

- -

- Special lemmas for squares. -

- -
-Lemma sqr_ge0 x : 0 ≤ x ^+ 2.
- -
-Lemma sqr_norm_eq1 x : (x ^+ 2 == 1) = (`|x | == 1).
- -
-Lemma lerif_mean_square_scaled x y :
- x × y *+ 2 ≤ x ^+ 2 + y ^+ 2 ?= iff (x == y ).
- -
-Lemma lerif_AGM2_scaled x y : x × y *+ 4 ≤ (x + y ) ^+ 2 ?= iff (x == y ).
- -
-Section MinMax.
- -
-

- -

- GG: Many of the first lemmas hold unconditionally, and others hold for - the real subset of a general domain. -

-Lemma minrC : @commutative R R min.
- -
-Lemma minrr : @idempotent R min.
- -
-Lemma minr_l x y : x ≤ y → min x y = x.
- -
-Lemma minr_r x y : y ≤ x → min x y = y.
- -
-Lemma maxrC : @commutative R R max.
- -
-Lemma maxrr : @idempotent R max.
- -
-Lemma maxr_l x y : y ≤ x → max x y = x.
- -
-Lemma maxr_r x y : x ≤ y → max x y = y.
- -
-Lemma addr_min_max x y : min x y + max x y = x + y.
- -
-Lemma addr_max_min x y : max x y + min x y = x + y.
- -
-Lemma minr_to_max x y : min x y = x + y - max x y.
- -
-Lemma maxr_to_min x y : max x y = x + y - min x y.
- -
-Lemma minrA x y z : min x (min y z) = min (min x y) z.
- -
-Lemma minrCA : @left_commutative R R min.
- -
-Lemma minrAC : @right_commutative R R min.
- -
-Variant minr_spec x y : bool → bool → R → Type :=
-| Minr_r of x ≤ y : minr_spec x y true false x
-| Minr_l of y < x : minr_spec x y false true y.
- -
-Lemma minrP x y : minr_spec x y (x ≤ y) (y < x) (min x y).
- -
-Lemma oppr_max x y : - max x y = min (- x) (- y).
- -
-Lemma oppr_min x y : - min x y = max (- x) (- y).
- -
-Lemma maxrA x y z : max x (max y z) = max (max x y) z.
- -
-Lemma maxrCA : @left_commutative R R max.
- -
-Lemma maxrAC : @right_commutative R R max.
- -
-Variant maxr_spec x y : bool → bool → R → Type :=
-| Maxr_r of y ≤ x : maxr_spec x y true false x
-| Maxr_l of x < y : maxr_spec x y false true y.
- -
-Lemma maxrP x y : maxr_spec x y (y ≤ x) (x < y) (maxr x y).
- -
-Lemma eqr_minl x y : (min x y == x ) = (x ≤ y ).
- -
-Lemma eqr_minr x y : (min x y == y ) = (y ≤ x ).
- -
-Lemma eqr_maxl x y : (max x y == x ) = (y ≤ x ).
- -
-Lemma eqr_maxr x y : (max x y == y ) = (x ≤ y ).
- -
-Lemma ler_minr x y z : (x ≤ min y z ) = (x ≤ y ) && (x ≤ z ).
- -
-Lemma ler_minl x y z : (min y z ≤ x ) = (y ≤ x ) || (z ≤ x ).
- -
-Lemma ler_maxr x y z : (x ≤ max y z ) = (x ≤ y ) || (x ≤ z ).
- -
-Lemma ler_maxl x y z : (max y z ≤ x ) = (y ≤ x ) && (z ≤ x ).
- -
-Lemma ltr_minr x y z : (x < min y z ) = (x < y ) && (x < z ).
- -
-Lemma ltr_minl x y z : (min y z < x ) = (y < x ) || (z < x ).
- -
-Lemma ltr_maxr x y z : (x < max y z ) = (x < y ) || (x < z ).
- -
-Lemma ltr_maxl x y z : (max y z < x ) = (y < x ) && (z < x ).
- -
-Definition lter_minr := (ler_minr , ltr_minr ).
-Definition lter_minl := (ler_minl , ltr_minl ).
-Definition lter_maxr := (ler_maxr , ltr_maxr ).
-Definition lter_maxl := (ler_maxl , ltr_maxl ).
- -
-Lemma addr_minl : @left_distributive R R +%R min.
- -
-Lemma addr_minr : @right_distributive R R +%R min.
- -
-Lemma addr_maxl : @left_distributive R R +%R max.
- -
-Lemma addr_maxr : @right_distributive R R +%R max.
- -
-Lemma minrK x y : max (min x y) x = x.
- -
-Lemma minKr x y : min y (max x y) = y.
- -
-Lemma maxr_minl : @left_distributive R R max min.
- -
-Lemma maxr_minr : @right_distributive R R max min.
- -
-Lemma minr_maxl : @left_distributive R R min max.
- -
-Lemma minr_maxr : @right_distributive R R min max.
- -
-Lemma minr_pmulr x y z : 0 ≤ x → x × min y z = min (x × y) (x × z).
- -
-Lemma minr_nmulr x y z : x ≤ 0 → x × min y z = max (x × y) (x × z).
- -
-Lemma maxr_pmulr x y z : 0 ≤ x → x × max y z = max (x × y) (x × z).
- -
-Lemma maxr_nmulr x y z : x ≤ 0 → x × max y z = min (x × y) (x × z).
- -
-Lemma minr_pmull x y z : 0 ≤ x → min y z × x = min (y × x) (z × x).
- -
-Lemma minr_nmull x y z : x ≤ 0 → min y z × x = max (y × x) (z × x).
- -
-Lemma maxr_pmull x y z : 0 ≤ x → max y z × x = max (y × x) (z × x).
- -
-Lemma maxr_nmull x y z : x ≤ 0 → max y z × x = min (y × x) (z × x).
- -
-Lemma maxrN x : max x (- x) = `|x |.
- -
-Lemma maxNr x : max (- x) x = `|x |.
- -
-Lemma minrN x : min x (- x) = - `|x |.
- -
-Lemma minNr x : min (- x) x = - `|x |.
- -
-End MinMax.
- -
-Section PolyBounds.
- -
-Variable p : {poly R }.
- -
-Lemma poly_itv_bound a b : {ub | ∀ x, a ≤ x ≤ b → `|p .[x ]| ≤ ub }.
- -
-Lemma monic_Cauchy_bound : p \is monic → {b | ∀ x, x ≥ b → p .[x ] > 0}.
- -
-End PolyBounds.
- -
-End RealDomainOperations.
- -
-Section RealField.
- -
-Variables (F : realFieldType) (x y : F).
- -
-Lemma lerif_mean_square : x × y ≤ (x ^+ 2 + y ^+ 2) / 2%:R ?= iff (x == y ).
- -
-Lemma lerif_AGM2 : x × y ≤ ((x + y ) / 2%:R )^+ 2 ?= iff (x == y ).
- -
-End RealField.
- -
-Section ArchimedeanFieldTheory.
- -
-Variables (F : archiFieldType) (x : F).
- -
-Lemma archi_boundP : 0 ≤ x → x < (bound x )%:R.
- -
-Lemma upper_nthrootP i : (bound x ≤ i)%N → x < 2%:R ^+ i.
- -
-End ArchimedeanFieldTheory.
- -
-Section RealClosedFieldTheory.
- -
-Variable R : rcfType.
-Implicit Types a x y : R.
- -
-Lemma poly_ivt : real_closed_axiom R.
- -
-

- -

- Square Root theory -

- -
-Lemma sqrtr_ge0 a : 0 ≤ sqrt a.
- Hint Resolve sqrtr_ge0 : core.
- -
-Lemma sqr_sqrtr a : 0 ≤ a → sqrt a ^+ 2 = a.
- -
-Lemma ler0_sqrtr a : a ≤ 0 → sqrt a = 0.
- -
-Lemma ltr0_sqrtr a : a < 0 → sqrt a = 0.
- -
-Variant sqrtr_spec a : R → bool → bool → R → Type :=
-| IsNoSqrtr of a < 0 : sqrtr_spec a a false true 0
-| IsSqrtr b of 0 ≤ b : sqrtr_spec a (b ^+ 2) true false b.
- -
-Lemma sqrtrP a : sqrtr_spec a a (0 ≤ a) (a < 0) (sqrt a).
- -
-Lemma sqrtr_sqr a : sqrt (a ^+ 2) = `|a |.
- -
-Lemma sqrtrM a b : 0 ≤ a → sqrt (a × b) = sqrt a × sqrt b.
- -
-Lemma sqrtr0 : sqrt 0 = 0 :> R.
- -
-Lemma sqrtr1 : sqrt 1 = 1 :> R.
- -
-Lemma sqrtr_eq0 a : (sqrt a == 0) = (a ≤ 0).
- -
-Lemma sqrtr_gt0 a : (0 < sqrt a ) = (0 < a ).
- -
-Lemma eqr_sqrt a b : 0 ≤ a → 0 ≤ b → (sqrt a == sqrt b ) = (a == b ).
- -
-Lemma ler_wsqrtr : {homo @sqrt R : a b / a ≤ b }.
- -
-Lemma ler_psqrt : {in @pos R &, {mono sqrt : a b / a ≤ b }}.
- -
-Lemma ler_sqrt a b : 0 < b → (sqrt a ≤ sqrt b ) = (a ≤ b ).
- -
-Lemma ltr_sqrt a b : 0 < b → (sqrt a < sqrt b ) = (a < b ).
- -
-End RealClosedFieldTheory.
- -
-Definition conjC {C : numClosedFieldType} : {rmorphism C → C } :=
- ClosedField.conj_op (ClosedField.conj_mixin (ClosedField.class C)).
-Notation "z ^*" := (@conjC _ z) (at level 2, format "z ^*") : ring_scope.
- -
-Definition imaginaryC {C : numClosedFieldType} : C :=
- ClosedField.imaginary (ClosedField.conj_mixin (ClosedField.class C)).
-Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope.
- -
-Section ClosedFieldTheory.
- -
-Variable C : numClosedFieldType.
-Implicit Types a x y z : C.
- -
-Definition normCK x : `|x | ^+ 2 = x × x ^*.
- -
-Lemma sqrCi : 'i ^+ 2 = -1 :> C.
- -
-Lemma conjCK : involutive (@conjC C).
- -
-Let Re2 z := z + z ^*.
-Definition nnegIm z := (0 ≤ imaginaryC × (z ^* - z )).
-Definition argCle y z := nnegIm z ==> nnegIm y && (Re2 z ≤ Re2 y ).
- -
-Variant rootC_spec n (x : C) : Type :=
- RootCspec (y : C) of if (n > 0)%N then y ^+ n = x else y = 0
- & ∀ z, (n > 0)%N → z ^+ n = x → argCle y z.
- -
-Fact rootC_subproof n x : rootC_spec n x.
- -
-Definition nthroot n x := let: RootCspec y _ _ := rootC_subproof n x in y.
-Notation "n .-root" := (nthroot n) (at level 2, format "n .-root") : ring_core_scope.
-Notation "n .-root" := (nthroot n) (only parsing) : ring_scope.
-Notation sqrtC := 2.-root.
- -
-Definition Re x := (x + x ^*) / 2%:R.
-Definition Im x := 'i × (x ^* - x ) / 2%:R.
-Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope.
-Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope.
- -
-Let nz2 : 2%:R != 0 :> C.
- -
-Lemma normCKC x : `|x | ^+ 2 = x ^* × x.
- -
-Lemma mul_conjC_ge0 x : 0 ≤ x × x ^*.
- -
-Lemma mul_conjC_gt0 x : (0 < x × x ^*) = (x != 0).
- -
-Lemma mul_conjC_eq0 x : (x × x ^* == 0) = (x == 0).
- -
-Lemma conjC_ge0 x : (0 ≤ x ^*) = (0 ≤ x ).
- -
-Lemma conjC_nat n : (n %:R )^* = n %:R :> C.
-Lemma conjC0 : 0^* = 0 :> C.
-Lemma conjC1 : 1^* = 1 :> C.
-Lemma conjC_eq0 x : (x ^* == 0) = (x == 0).
- -
-Lemma invC_norm x : x ^-1 = `|x | ^- 2 × x ^*.
- -
-

- -

- Real number subset. -

- -
-Lemma CrealE x : (x \is real ) = (x ^* == x ).
- -
-Lemma CrealP {x} : reflect (x ^* = x) (x \is real).
- -
-Lemma conj_Creal x : x \is real → x ^* = x.
- -
-Lemma conj_normC z : `|z |^* = `|z |.
- -
-Lemma geC0_conj x : 0 ≤ x → x ^* = x.
- -
-Lemma geC0_unit_exp x n : 0 ≤ x → (x ^+ n .+1 == 1) = (x == 1).
- -
-

- -

- Elementary properties of roots. -

- -
-Ltac case_rootC := rewrite /nthroot; case: (rootC_subproof _ _).
- -
-Lemma root0C x : 0.-root x = 0.
- -
-Lemma rootCK n : (n > 0)%N → cancel n .-root (fun x ⇒ x ^+ n).
- -
-Lemma root1C x : 1.-root x = x.
- -
-Lemma rootC0 n : n .-root 0 = 0.
- -
-Lemma rootC_inj n : (n > 0)%N → injective n .-root.
- -
-Lemma eqr_rootC n : (n > 0)%N → {mono n .-root : x y / x == y }.
- -
-Lemma rootC_eq0 n x : (n > 0)%N → (n .-root x == 0) = (x == 0).
- -
-

- -

- Rectangular coordinates. -

- -
-Lemma nonRealCi : ('i : C ) \isn't real.
- -
-Lemma neq0Ci : 'i != 0 :> C.
- -
-Lemma normCi : `|'i | = 1 :> C.
- -
-Lemma invCi : 'i ^-1 = - 'i :> C.
- -
-Lemma conjCi : 'i ^* = - 'i :> C.
- -
-Lemma Crect x : x = 'Re x + 'i × 'Im x.
- -
-Lemma Creal_Re x : 'Re x \is real.
- -
-Lemma Creal_Im x : 'Im x \is real.
-Hint Resolve Creal_Re Creal_Im : core.
- -
-Fact Re_is_additive : additive Re.
- Canonical Re_additive := Additive Re_is_additive.
- -
-Fact Im_is_additive : additive Im.
-Canonical Im_additive := Additive Im_is_additive.
- -
-Lemma Creal_ImP z : reflect ('Im z = 0) (z \is real).
- -
-Lemma Creal_ReP z : reflect ('Re z = z) (z \in real).
- -
-Lemma ReMl : {in real , ∀ x, {morph Re : z / x × z }}.
- -
-Lemma ReMr : {in real , ∀ x, {morph Re : z / z × x }}.
- -
-Lemma ImMl : {in real , ∀ x, {morph Im : z / x × z }}.
- -
-Lemma ImMr : {in real , ∀ x, {morph Im : z / z × x }}.
- -
-Lemma Re_i : 'Re 'i = 0.
- -
-Lemma Im_i : 'Im 'i = 1.
- -
-Lemma Re_conj z : 'Re z ^* = 'Re z.
- -
-Lemma Im_conj z : 'Im z ^* = - 'Im z.
- -
-Lemma Re_rect : {in real &, ∀ x y, 'Re (x + 'i × y ) = x }.
- -
-Lemma Im_rect : {in real &, ∀ x y, 'Im (x + 'i × y ) = y }.
- -
-Lemma conjC_rect : {in real &, ∀ x y, (x + 'i × y )^* = x - 'i × y }.
- -
-Lemma addC_rect x1 y1 x2 y2 :
-  (x1 + 'i × y1 ) + (x2 + 'i × y2 ) = x1 + x2 + 'i × (y1 + y2 ).
- -
-Lemma oppC_rect x y : - (x + 'i × y ) = - x + 'i × (- y ).
- -
-Lemma subC_rect x1 y1 x2 y2 :
-  (x1 + 'i × y1 ) - (x2 + 'i × y2 ) = x1 - x2 + 'i × (y1 - y2 ).
- -
-Lemma mulC_rect x1 y1 x2 y2 :
-  (x1 + 'i × y1 ) × (x2 + 'i × y2 )
-      = x1 × x2 - y1 × y2 + 'i × (x1 × y2 + x2 × y1 ).
- -
-Lemma normC2_rect :
-  {in real &, ∀ x y, `|x + 'i × y | ^+ 2 = x ^+ 2 + y ^+ 2}.
- -
-Lemma normC2_Re_Im z : `|z | ^+ 2 = 'Re z ^+ 2 + 'Im z ^+ 2.
- -
-Lemma invC_rect :
-  {in real &, ∀ x y, (x + 'i × y )^-1 = (x - 'i × y ) / (x ^+ 2 + y ^+ 2)}.
- -
-Lemma lerif_normC_Re_Creal z : `|'Re z | ≤ `|z | ?= iff (z \is real ).
- -
-Lemma lerif_Re_Creal z : 'Re z ≤ `|z | ?= iff (0 ≤ z ).
- -
-

- -

- Equality from polar coordinates, for the upper plane. -

-Lemma eqC_semipolar x y :
- `|x | = `|y | → 'Re x = 'Re y → 0 ≤ 'Im x × 'Im y → x = y.
- -
-

- -

- Nth roots. -

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

- -

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

- -
-Lemma rootC_Re_max n x y :
- (n > 0)%N → y ^+ n = x → 0 ≤ 'Im y → 'Re y ≤ 'Re (n .-root x ).
- -
-Let neg_unity_root n : (n > 1)%N → exists2 w : C , w ^+ n = 1 & 'Re w < 0.
- -
-Lemma Im_rootC_ge0 n x : (n > 1)%N → 0 ≤ 'Im (n .-root x ).
- -
-Lemma rootC_lt0 n x : (1 < n)%N → (n .-root x < 0) = false.
- -
-Lemma rootC_ge0 n x : (n > 0)%N → (0 ≤ n .-root x ) = (0 ≤ x ).
- -
-Lemma rootC_gt0 n x : (n > 0)%N → (n .-root x > 0) = (x > 0).
- -
-Lemma rootC_le0 n x : (1 < n)%N → (n .-root x ≤ 0) = (x == 0).
- -
-Lemma ler_rootCl n : (n > 0)%N → {in Num.nneg , {mono n .-root : x y / x ≤ y }}.
- -
-Lemma ler_rootC n : (n > 0)%N → {in Num.nneg &, {mono n .-root : x y / x ≤ y }}.
- -
-Lemma ltr_rootCl n : (n > 0)%N → {in Num.nneg , {mono n .-root : x y / x < y }}.
- -
-Lemma ltr_rootC n : (n > 0)%N → {in Num.nneg &, {mono n .-root : x y / x < y }}.
- -
-Lemma exprCK n x : (0 < n)%N → 0 ≤ x → n .-root (x ^+ n) = x.
- -
-Lemma norm_rootC n x : `|n .-root x | = n .-root `|x |.
- -
-Lemma rootCX n x k : (n > 0)%N → 0 ≤ x → n .-root (x ^+ k) = n .-root x ^+ k.
- -
-Lemma rootC1 n : (n > 0)%N → n .-root 1 = 1.
- -
-Lemma rootCpX n x k : (k > 0)%N → 0 ≤ x → n .-root (x ^+ k) = n .-root x ^+ k.
- -
-Lemma rootCV n x : (n > 0)%N → 0 ≤ x → n .-root x ^-1 = (n .-root x )^-1.
- -
-Lemma rootC_eq1 n x : (n > 0)%N → (n .-root x == 1) = (x == 1).
- -
-Lemma rootC_ge1 n x : (n > 0)%N → (n .-root x ≥ 1) = (x ≥ 1).
- -
-Lemma rootC_gt1 n x : (n > 0)%N → (n .-root x > 1) = (x > 1).
- -
-Lemma rootC_le1 n x : (n > 0)%N → 0 ≤ x → (n .-root x ≤ 1) = (x ≤ 1).
- -
-Lemma rootC_lt1 n x : (n > 0)%N → 0 ≤ x → (n .-root x < 1) = (x < 1).
- -
-Lemma rootCMl n x z : 0 ≤ x → n .-root (x × z) = n .-root x × n .-root z.
- -
-Lemma rootCMr n x z : 0 ≤ x → n .-root (z × x) = n .-root z × n .-root x.
- -
-Lemma imaginaryCE : 'i = sqrtC (-1).
- -
-

- -

- More properties of n.-root will be established in cyclotomic.v. -

- - The proper form of the Arithmetic - Geometric Mean inequality. -

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

- -

- Square root. -

- -
-Lemma sqrtC0 : sqrtC 0 = 0.
-Lemma sqrtC1 : sqrtC 1 = 1.
-Lemma sqrtCK x : sqrtC x ^+ 2 = x.
-Lemma sqrCK x : 0 ≤ x → sqrtC (x ^+ 2) = x.
- -
-Lemma sqrtC_ge0 x : (0 ≤ sqrtC x ) = (0 ≤ x ).
-Lemma sqrtC_eq0 x : (sqrtC x == 0) = (x == 0).
-Lemma sqrtC_gt0 x : (sqrtC x > 0) = (x > 0).
-Lemma sqrtC_lt0 x : (sqrtC x < 0) = false.
-Lemma sqrtC_le0 x : (sqrtC x ≤ 0) = (x == 0).
- -
-Lemma ler_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x ≤ y }}.
- Lemma ltr_sqrtC : {in Num.nneg &, {mono sqrtC : x y / x < y }}.
- Lemma eqr_sqrtC : {mono sqrtC : x y / x == y }.
- Lemma sqrtC_inj : injective sqrtC.
- Lemma sqrtCM : {in Num.nneg &, {morph sqrtC : x y / x × y }}.
- -
-Lemma sqrCK_P x : reflect (sqrtC (x ^+ 2) = x) ((0 ≤ 'Im x ) && ~~ (x < 0)).
- -
-Lemma normC_def x : `|x | = sqrtC (x × x ^*).
- -
-Lemma norm_conjC x : `|x ^*| = `|x |.
- -
-Lemma normC_rect :
- {in real &, ∀ x y, `|x + 'i × y | = sqrtC (x ^+ 2 + y ^+ 2)}.
- -
-Lemma normC_Re_Im z : `|z | = sqrtC ('Re z ^+ 2 + 'Im z ^+ 2).
- -
-

- -

- Norm sum (in)equalities. -

- -
-Lemma normC_add_eq x y :
-    `|x + y | = `|x | + `|y | →
-  {t : C | `|t | == 1 & (x , y ) = (`|x | × t , `|y | × t )}.
- -
-Lemma normC_sum_eq (I : finType) (P : pred I) (F : I → C) :
-     `|\sum_(i | P i ) F i | = \sum_(i | P i ) `|F i | →
-   {t : C | `|t | == 1 & ∀ i, P i → F i = `|F i | × t }.
- -
-Lemma normC_sum_eq1 (I : finType) (P : pred I) (F : I → C) :
-    `|\sum_(i | P i ) F i | = (\sum_(i | P i ) `|F i |) →
-     (∀ i, P i → `|F i | = 1) →
-   {t : C | `|t | == 1 & ∀ i, P i → F i = t }.
- -
-Lemma normC_sum_upper (I : finType) (P : pred I) (F G : I → C) :
-     (∀ i, P i → `|F i | ≤ G i ) →
-     \sum_(i | P i ) F i = \sum_(i | P i ) G i →
-   ∀ i, P i → F i = G i.
- -
-Lemma normC_sub_eq x y :
-  `|x - y | = `|x | - `|y | → {t | `|t | == 1 & (x , y ) = (`|x | × t , `|y | × t )}.
- -
-End ClosedFieldTheory.
- -
-Notation "n .-root" := (@nthroot _ n)
-  (at level 2, format "n .-root") : ring_scope.
-Notation sqrtC := 2.-root.
-Notation "'i" := (@imaginaryC _) (at level 0) : ring_scope.
-Notation "'Re z" := (Re z) (at level 10, z at level 8) : ring_scope.
-Notation "'Im z" := (Im z) (at level 10, z at level 8) : ring_scope.
- -
- -
-End Theory.
- -
-Module RealMixin.
- -
-Section RealMixins.
- -
-Variables (R : idomainType) (le : rel R) (lt : rel R) (norm : R → R).
- -
-Section LeMixin.
- -
-Hypothesis le0_add : ∀ x y, 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
-Hypothesis le0_mul : ∀ x y, 0 ≤ x → 0 ≤ y → 0 ≤ x × y.
-Hypothesis le0_anti : ∀ x, 0 ≤ x → x ≤ 0 → x = 0.
-Hypothesis sub_ge0 : ∀ x y, (0 ≤ y - x ) = (x ≤ y ).
-Hypothesis le0_total : ∀ x, (0 ≤ x ) || (x ≤ 0).
-Hypothesis normN: ∀ x, `|- x | = `|x |.
-Hypothesis ge0_norm : ∀ x, 0 ≤ x → `|x | = x.
-Hypothesis lt_def : ∀ x y, (x < y ) = (y != x ) && (x ≤ y ).
- -
-Let le0N x : (0 ≤ - x ) = (x ≤ 0).
-Let leN_total x : 0 ≤ x ∨ 0 ≤ - x.
- -
-Let le00 : (0 ≤ 0).
-Let le01 : (0 ≤ 1).
- -
-Fact lt0_add x y : 0 < x → 0 < y → 0 < x + y.
- -
-Fact eq0_norm x : `|x | = 0 → x = 0.
- -
-Fact le_def x y : (x ≤ y ) = (`|y - x | == y - x ).
- -
-Fact normM : {morph norm : x y / x × y }.
- -
-Fact le_normD x y : `|x + y | ≤ `|x | + `|y |.
- -
-Lemma le_total x y : (x ≤ y ) || (y ≤ x ).
- -
-Definition Le :=
-  Mixin le_normD lt0_add eq0_norm (in2W le_total) normM le_def lt_def.
- -
-Lemma Real (R' : numDomainType) & phant R' :
-  R' = NumDomainType R Le → real_axiom R'.
- -
-End LeMixin.
- -
-Section LtMixin.
- -
-Hypothesis lt0_add : ∀ x y, 0 < x → 0 < y → 0 < x + y.
-Hypothesis lt0_mul : ∀ x y, 0 < x → 0 < y → 0 < x × y.
-Hypothesis lt0_ngt0 : ∀ x, 0 < x → ~~ (x < 0).
-Hypothesis sub_gt0 : ∀ x y, (0 < y - x ) = (x < y ).
-Hypothesis lt0_total : ∀ x, x != 0 → (0 < x ) || (x < 0).
-Hypothesis normN : ∀ x, `|- x | = `|x |.
-Hypothesis ge0_norm : ∀ x, 0 ≤ x → `|x | = x.
-Hypothesis le_def : ∀ x y, (x ≤ y ) = (y == x ) || (x < y ).
- -
-Fact le0_add x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
- -
-Fact le0_mul x y : 0 ≤ x → 0 ≤ y → 0 ≤ x × y.
- -
-Fact le0_anti x : 0 ≤ x → x ≤ 0 → x = 0.
- -
-Fact sub_ge0 x y : (0 ≤ y - x ) = (x ≤ y ).
- -
-Fact lt_def x y : (x < y ) = (y != x ) && (x ≤ y ).
- -
-Fact le0_total x : (0 ≤ x ) || (x ≤ 0).
- -
-Definition Lt :=
-  Le le0_add le0_mul le0_anti sub_ge0 le0_total normN ge0_norm lt_def.
- -
-End LtMixin.
- -
-End RealMixins.
- -
-End RealMixin.
- -
-End Num.
- -
-Export Num.NumDomain.Exports Num.NumField.Exports Num.ClosedField.Exports.
-Export Num.RealDomain.Exports Num.RealField.Exports.
-Export Num.ArchimedeanField.Exports Num.RealClosedField.Exports.
-Export Num.Syntax Num.PredInstances.
- -
-Notation RealLeMixin := Num.RealMixin.Le.
-Notation RealLtMixin := Num.RealMixin.Lt.
-Notation RealLeAxiom R := (Num.RealMixin.Real (Phant R) (erefl _)).
-Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin.
-