Library Coq.Reals.ConstructiveRIneq


Basic lemmas for the contructive real numbers



Require Import ConstructiveCauchyReals.
Require Import ConstructiveRcomplete.
Require Import ConstructiveRealsLUB.
Require Export ConstructiveReals.
Require Import Zpower.
Require Export ZArithRing.
Require Import Omega.
Require Import QArith_base.
Require Import Qring.


Local Open Scope Z_scope.
Local Open Scope R_scope_constr.

Definition CR : ConstructiveReals.

Definition R := CRcarrier CR.

Definition Req := orderEq R (CRlt CR).
Definition Rle (x y : R) := CRlt CR y x -> False.
Definition Rge (x y : R) := CRlt CR x y -> False.
Definition Rlt := CRlt CR.
Definition RltProp := CRltProp CR.
Definition Rgt (x y : R) := CRlt CR y x.
Definition Rappart := orderAppart R (CRlt CR).

Infix "==" := Req : R_scope_constr.
Infix "#" := Rappart : R_scope_constr.
Infix "<" := Rlt : R_scope_constr.
Infix ">" := Rgt : R_scope_constr.
Infix "<=" := Rle : R_scope_constr.
Infix ">=" := Rge : R_scope_constr.

Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope_constr.
Notation "x <= y < z" := (prod (x <= y) (y < z)) : R_scope_constr.
Notation "x < y < z" := (prod (x < y) (y < z)) : R_scope_constr.
Notation "x < y <= z" := (prod (x < y) (y <= z)) : R_scope_constr.

Lemma Rlt_epsilon : forall x y : R, RltProp x y -> x < y.

Lemma Rlt_forget : forall x y : R, x < y -> RltProp x y.

Lemma Rle_refl : forall x : R, x <= x.
Hint Immediate Rle_refl: rorders.

Lemma Req_refl : forall x : R, x == x.

Lemma Req_sym : forall x y : R, x == y -> y == x.

Lemma Req_trans : forall x y z : R, x == y -> y == z -> x == z.

Add Parametric Relation : R Req
    reflexivity proved by Req_refl
    symmetry proved by Req_sym
    transitivity proved by Req_trans
      as Req_rel.

Instance Req_relT : CRelationClasses.Equivalence Req.

Lemma linear_order_T : forall x y z : R,
    x < z -> (x < y) + (y < z).

Instance Rlt_morph
  : CMorphisms.Proper
      (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rlt.

Instance RltProp_morph
  : Morphisms.Proper
      (Morphisms.respectful Req (Morphisms.respectful Req iff)) RltProp.

Instance Rgt_morph
  : CMorphisms.Proper
      (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rgt.

Instance Rappart_morph
  : CMorphisms.Proper
      (CMorphisms.respectful Req (CMorphisms.respectful Req CRelationClasses.iffT)) Rappart.

Add Parametric Morphism : Rle
    with signature Req ==> Req ==> iff
      as Rle_morph.

Add Parametric Morphism : Rge
    with signature Req ==> Req ==> iff
      as Rge_morph.

Definition Rplus := CRplus CR.
Definition Rmult := CRmult CR.
Definition Rinv := CRinv CR.
Definition Ropp := CRopp CR.

Add Parametric Morphism : Rplus
    with signature Req ==> Req ==> Req
      as Rplus_morph.

Instance Rplus_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rplus.

Add Parametric Morphism : Rmult
    with signature Req ==> Req ==> Req
      as Rmult_morph.

Instance Rmult_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful Req (CMorphisms.respectful Req Req)) Rmult.

Add Parametric Morphism : Ropp
    with signature Req ==> Req
      as Ropp_morph.

Instance Ropp_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful Req Req) Ropp.

Infix "+" := Rplus : R_scope_constr.
Notation "- x" := (Ropp x) : R_scope_constr.
Definition Rminus (r1 r2:R) : R := r1 + - r2.
Infix "-" := Rminus : R_scope_constr.
Infix "*" := Rmult : R_scope_constr.
Notation "/ x" := (CRinv CR x) (at level 35, right associativity) : R_scope_constr.

Notation "0" := (CRzero CR) : R_scope_constr.
Notation "1" := (CRone CR) : R_scope_constr.

Add Parametric Morphism : Rminus
    with signature Req ==> Req ==> Req
      as Rminus_morph.

Lemma RisRing : ring_theory 0 1
                            Rplus Rmult
                            Rminus Ropp
                            Req.

Add Ring CRealRing : RisRing.

Lemma Rplus_comm : forall x y:R, x + y == y + x.

Lemma Rplus_assoc : forall x y z:R, (x + y) + z == x + (y + z).

Lemma Rplus_opp_r : forall x:R, x + -x == 0.

Lemma Rplus_0_l : forall x:R, 0 + x == x.

Lemma Rmult_0_l : forall x:R, 0 * x == 0.

Lemma Rmult_1_l : forall x:R, 1 * x == x.

Lemma Rmult_comm : forall x y:R, x * y == y * x.

Lemma Rmult_assoc : forall x y z:R, (x * y) * z == x * (y * z).

Definition Rinv_l := CRinv_l CR.

Lemma Rmult_plus_distr_l : forall r1 r2 r3 : R,
    r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).

Definition Rlt_0_1 := CRzero_lt_one CR.

Lemma Rlt_asym : forall x y :R, x < y -> y < x -> False.

Lemma Rlt_trans : forall x y z : R, x < y -> y < z -> x < z.

Lemma Rplus_lt_compat_l : forall x y z : R,
    y < z -> x + y < x + z.

Lemma Ropp_mult_distr_l
  : forall r1 r2 : R, -(r1 * r2) == (- r1) * r2.

Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.

Lemma Rmult_lt_compat_l : forall x y z : R,
    0 < x -> y < z -> x * y < x * z.

Hint Resolve Rplus_comm Rplus_assoc Rplus_opp_r Rplus_0_l
     Rmult_comm Rmult_assoc Rinv_l Rmult_1_l Rmult_plus_distr_l
     Rlt_0_1 Rlt_asym Rlt_trans Rplus_lt_compat_l Rmult_lt_compat_l
     Rmult_0_l : creal.

Fixpoint INR (n:nat) : R :=
  match n with
  | O => 0
  | S O => 1
  | S n => INR n + 1
  end.

Fixpoint IPR_2 (p:positive) : R :=
  match p with
  | xH => 1 + 1
  | xO p => (1 + 1) * IPR_2 p
  | xI p => (1 + 1) * (1 + IPR_2 p)
  end.

Definition IPR (p:positive) : R :=
  match p with
  | xH => 1
  | xO p => IPR_2 p
  | xI p => 1 + IPR_2 p
  end.

Definition IZR (z:Z) : R :=
  match z with
  | Z0 => 0
  | Zpos n => IPR n
  | Zneg n => - IPR n
  end.

Notation "2" := (IZR 2) : R_scope_constr.

Relation between orders and equality


Lemma Rge_refl : forall r, r <= r.
Hint Immediate Rge_refl: rorders.

Irreflexivity of the strict order

Lemma Rlt_irrefl : forall r, r < r -> False.
Hint Resolve Rlt_irrefl: creal.

Lemma Rgt_irrefl : forall r, r > r -> False.

Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2.

Lemma Rgt_not_eq : forall r1 r2, r1 > r2 -> r1 <> r2.

Lemma Rlt_dichotomy_converse : forall r1 r2, ((r1 < r2) + (r1 > r2)) -> r1 <> r2.
Hint Resolve Rlt_dichotomy_converse: creal.

Reasoning by case on equality and order

Relating <, >, <= and >=

Order

Relating strict and large orders


Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
Hint Resolve Rlt_le: creal.

Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2.

Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1.
Hint Immediate Rle_ge: creal.
Hint Resolve Rle_ge: rorders.

Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1.
Hint Resolve Rge_le: creal.
Hint Immediate Rge_le: rorders.

Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1.
Hint Resolve Rlt_gt: rorders.

Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1.
Hint Immediate Rgt_lt: rorders.


Lemma Rnot_lt_le : forall r1 r2, (r1 < r2 -> False) -> r2 <= r1.

Lemma Rnot_gt_le : forall r1 r2, (r1 > r2 -> False) -> r1 <= r2.

Lemma Rnot_gt_ge : forall r1 r2, (r1 > r2 -> False) -> r2 >= r1.

Lemma Rnot_lt_ge : forall r1 r2, (r1 < r2 -> False) -> r1 >= r2.

Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
Hint Immediate Rlt_not_le: creal.

Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2.

Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2.
Hint Immediate Rlt_not_ge: creal.

Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2.

Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> r1 < r2 -> False.

Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> r1 < r2 -> False.

Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> r1 > r2 -> False.

Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> r1 > r2 -> False.

Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2.
Hint Immediate Req_le: creal.

Lemma Req_ge : forall r1 r2, r1 = r2 -> r1 >= r2.
Hint Immediate Req_ge: creal.

Lemma Req_le_sym : forall r1 r2, r2 = r1 -> r1 <= r2.
Hint Immediate Req_le_sym: creal.

Lemma Req_ge_sym : forall r1 r2, r2 = r1 -> r1 >= r2.
Hint Immediate Req_ge_sym: creal.

Asymmetry

Remark: Rlt_asym is an axiom

Lemma Rgt_asym : forall r1 r2, r1 > r2 -> r2 > r1 -> False.

Compatibility with equality


Lemma Rlt_eq_compat :
  forall r1 r2 r3 r4, r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3.

Lemma Rgt_eq_compat :
  forall r1 r2 r3 r4, r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3.

Transitivity


Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3.

Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3.

Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3.

Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3.

Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3.

Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3.

Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3.

Addition

Remark: Rplus_0_l is an axiom

Lemma Rplus_0_r : forall r, r + 0 == r.
Hint Resolve Rplus_0_r: creal.

Lemma Rplus_ne : forall r, r + 0 == r /\ 0 + r == r.
Hint Resolve Rplus_ne: creal.


Remark: Rplus_opp_r is an axiom

Lemma Rplus_opp_l : forall r, - r + r == 0.
Hint Resolve Rplus_opp_l: creal.

Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 == 0 -> r2 == - r1.

Lemma Rplus_eq_compat_l : forall r r1 r2, r1 == r2 -> r + r1 == r + r2.

Lemma Rplus_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 + r == r2 + r.

Lemma Rplus_eq_reg_l : forall r r1 r2, r + r1 == r + r2 -> r1 == r2.
Hint Resolve Rplus_eq_reg_l: creal.

Lemma Rplus_eq_reg_r : forall r r1 r2, r1 + r == r2 + r -> r1 == r2.

Lemma Rplus_0_r_uniq : forall r r1, r + r1 == r -> r1 == 0.

Multiplication

Lemma Rinv_r : forall r (rnz : r # 0),
    r # 0 -> r * ((/ r) rnz) == 1.
Hint Resolve Rinv_r: creal.

Lemma Rinv_l_sym : forall r (rnz: r # 0), 1 == (/ r) rnz * r.
Hint Resolve Rinv_l_sym: creal.

Lemma Rinv_r_sym : forall r (rnz : r # 0), 1 == r * (/ r) rnz.
Hint Resolve Rinv_r_sym: creal.

Lemma Rmult_0_r : forall r, r * 0 == 0.
Hint Resolve Rmult_0_r: creal.

Lemma Rmult_ne : forall r, r * 1 == r /\ 1 * r == r.
Hint Resolve Rmult_ne: creal.

Lemma Rmult_1_r : forall r, r * 1 == r.
Hint Resolve Rmult_1_r: creal.

Lemma Rmult_eq_compat_l : forall r r1 r2, r1 == r2 -> r * r1 == r * r2.

Lemma Rmult_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 * r == r2 * r.

Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 == r * r2 -> r # 0 -> r1 == r2.

Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2.

Lemma Rmult_eq_0_compat : forall r1 r2, r1 == 0 \/ r2 == 0 -> r1 * r2 == 0.

Hint Resolve Rmult_eq_0_compat: creal.

Lemma Rmult_eq_0_compat_r : forall r1 r2, r1 == 0 -> r1 * r2 == 0.

Lemma Rmult_eq_0_compat_l : forall r1 r2, r2 == 0 -> r1 * r2 == 0.

Lemma Rmult_integral_contrapositive :
  forall r1 r2, (prod (r1 # 0) (r2 # 0)) -> (r1 * r2) # 0.
Hint Resolve Rmult_integral_contrapositive: creal.

Lemma Rmult_integral_contrapositive_currified :
  forall r1 r2, r1 # 0 -> r2 # 0 -> (r1 * r2) # 0.

Lemma Rmult_plus_distr_r :
  forall r1 r2 r3, (r1 + r2) * r3 == r1 * r3 + r2 * r3.

Square function

Definition Rsqr (r : R) := r * r.

Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope_constr.

Lemma Rsqr_0 : Rsqr 0 == 0.

Opposite

Lemma Ropp_eq_compat : forall r1 r2, r1 == r2 -> - r1 == - r2.
Hint Resolve Ropp_eq_compat: creal.

Lemma Ropp_0 : -0 == 0.
Hint Resolve Ropp_0: creal.

Lemma Ropp_eq_0_compat : forall r, r == 0 -> - r == 0.
Hint Resolve Ropp_eq_0_compat: creal.

Lemma Ropp_involutive : forall r, - - r == r.
Hint Resolve Ropp_involutive: creal.

Lemma Ropp_plus_distr : forall r1 r2, - (r1 + r2) == - r1 + - r2.
Hint Resolve Ropp_plus_distr: creal.

Opposite and multiplication


Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 == - (r1 * r2).
Hint Resolve Ropp_mult_distr_l_reverse: creal.

Lemma Rmult_opp_opp : forall r1 r2, - r1 * - r2 == r1 * r2.
Hint Resolve Rmult_opp_opp: creal.

Lemma Ropp_mult_distr_r : forall r1 r2, - (r1 * r2) == r1 * - r2.

Lemma Ropp_mult_distr_r_reverse : forall r1 r2, r1 * - r2 == - (r1 * r2).

Subtraction


Lemma Rminus_0_r : forall r, r - 0 == r.
Hint Resolve Rminus_0_r: creal.

Lemma Rminus_0_l : forall r, 0 - r == - r.
Hint Resolve Rminus_0_l: creal.

Lemma Ropp_minus_distr : forall r1 r2, - (r1 - r2) == r2 - r1.
Hint Resolve Ropp_minus_distr: creal.

Lemma Ropp_minus_distr' : forall r1 r2, - (r2 - r1) == r1 - r2.

Lemma Rminus_diag_eq : forall r1 r2, r1 == r2 -> r1 - r2 == 0.
Hint Resolve Rminus_diag_eq: creal.

Lemma Rminus_diag_uniq : forall r1 r2, r1 - r2 == 0 -> r1 == r2.
Hint Immediate Rminus_diag_uniq: creal.

Lemma Rminus_diag_uniq_sym : forall r1 r2, r2 - r1 == 0 -> r1 == r2.
Hint Immediate Rminus_diag_uniq_sym: creal.

Lemma Rplus_minus : forall r1 r2, r1 + (r2 - r1) == r2.
Hint Resolve Rplus_minus: creal.

Lemma Rmult_minus_distr_l :
  forall r1 r2 r3, r1 * (r2 - r3) == r1 * r2 - r1 * r3.

Order and addition

Compatibility

Remark: Rplus_lt_compat_l is an axiom

Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2.
Hint Resolve Rplus_gt_compat_l: creal.

Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r.
Hint Resolve Rplus_lt_compat_r: creal.

Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r.


Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2.

Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.

Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2.
Hint Resolve Rplus_ge_compat_l: creal.

Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r.

Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: creal.

Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r.

Lemma Rplus_lt_compat :
  forall r1 r2 r3 r4, r1 < r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
Hint Immediate Rplus_lt_compat: creal.

Lemma Rplus_le_compat :
  forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
Hint Immediate Rplus_le_compat: creal.

Lemma Rplus_gt_compat :
  forall r1 r2 r3 r4, r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4.

Lemma Rplus_ge_compat :
  forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4.

Lemma Rplus_lt_le_compat :
  forall r1 r2 r3 r4, r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4.

Lemma Rplus_le_lt_compat :
  forall r1 r2 r3 r4, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.

Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: creal.

Lemma Rplus_gt_ge_compat :
  forall r1 r2 r3 r4, r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4.

Lemma Rplus_ge_gt_compat :
  forall r1 r2 r3 r4, r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4.

Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2.

Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2.

Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.

Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.

Lemma sum_inequa_Rle_lt :
  forall a x b c y d,
    a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.

Cancellation


Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.

Lemma Rplus_le_reg_r : forall r r1 r2, r1 + r <= r2 + r -> r1 <= r2.

Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2.

Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2.

Lemma Rplus_le_reg_pos_r :
  forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3.

Lemma Rplus_lt_reg_pos_r : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3.

Lemma Rplus_ge_reg_neg_r :
  forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3.

Lemma Rplus_gt_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 > r3 -> r1 > r3.

Lemma Rplus_eq_0_l :
  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 == 0 -> r1 == 0.

Lemma Rplus_eq_R0 :
  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 == 0 -> r1 == 0 /\ r2 == 0.

Order and opposite

Contravariant compatibility


Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
Hint Resolve Ropp_gt_lt_contravar : creal.

Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
Hint Resolve Ropp_lt_gt_contravar: creal.

Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2.
Hint Resolve Ropp_lt_contravar: creal.

Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2.


Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
Hint Immediate Ropp_lt_cancel: creal.

Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2.

Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2.
Hint Resolve Ropp_le_ge_contravar: creal.

Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
Hint Resolve Ropp_ge_le_contravar: creal.

Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2.
Hint Resolve Ropp_le_contravar: creal.

Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2.

Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r.
Hint Resolve Ropp_0_lt_gt_contravar: creal.

Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r.
Hint Resolve Ropp_0_gt_lt_contravar: creal.

Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0.
Hint Resolve Ropp_lt_gt_0_contravar: creal.

Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0.
Hint Resolve Ropp_gt_lt_0_contravar: creal.

Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r.
Hint Resolve Ropp_0_le_ge_contravar: creal.

Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r.
Hint Resolve Ropp_0_ge_le_contravar: creal.

Cancellation


Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2.
Hint Immediate Ropp_le_cancel: creal.

Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2.

Order and multiplication

Remark: Rmult_lt_compat_l is an axiom

Covariant compatibility


Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
Hint Resolve Rmult_lt_compat_r : core.

Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r.

Lemma Rmult_gt_compat_l : forall r r1 r2, r > 0 -> r1 > r2 -> r * r1 > r * r2.

Lemma Rmult_gt_0_lt_compat :
  forall r1 r2 r3 r4,
    r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.

Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2.

Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0.

Contravariant compatibility


Lemma Rmult_lt_gt_compat_neg_l :
  forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2.

Cancellation


Lemma Rinv_0_lt_compat : forall r (rpos : 0 < r), 0 < (/ r) (inr rpos).

Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.

Lemma Rmult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2.

Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.

Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.

Lemma Rmult_le_reg_r : forall r r1 r2, 0 < r -> r1 * r <= r2 * r -> r1 <= r2.

Order and substraction


Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0.
Hint Resolve Rlt_minus: creal.

Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0.

Lemma Rlt_Rminus : forall a b, a < b -> 0 < b - a.

Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0.

Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.

Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2.

Lemma Rminus_gt : forall r1 r2, r1 - r2 > 0 -> r1 > r2.

Lemma Rminus_gt_0_lt : forall a b, 0 < b - a -> a < b.

Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2.

Lemma Rminus_ge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2.

Lemma tech_Rplus : forall r s, 0 <= r -> 0 < s -> r + s <> 0.
Hint Immediate tech_Rplus: creal.

Zero is less than one


Lemma Rle_0_1 : 0 <= 1.

Inverse


Lemma Rinv_1 : forall nz : 1 # 0, (/ 1) nz == 1.
Hint Resolve Rinv_1: creal.

Lemma Ropp_inv_permute : forall r (rnz : r # 0) (ronz : (-r) # 0),
    - (/ r) rnz == (/ - r) ronz.

Lemma Rinv_neq_0_compat : forall r (rnz : r # 0), ((/ r) rnz) # 0.
Hint Resolve Rinv_neq_0_compat: creal.

Lemma Rinv_involutive : forall r (rnz : r # 0) (rinz : ((/ r) rnz) # 0),
    (/ ((/ r) rnz)) rinz == r.
Hint Resolve Rinv_involutive: creal.

Lemma Rinv_mult_distr :
  forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1*r2) # 0),
    (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz.

Lemma Rinv_r_simpl_r : forall r1 r2 (rnz : r1 # 0), r1 * (/ r1) rnz * r2 == r2.

Lemma Rinv_r_simpl_l : forall r1 r2 (rnz : r1 # 0),
    r2 * r1 * (/ r1) rnz == r2.

Lemma Rinv_r_simpl_m : forall r1 r2 (rnz : r1 # 0),
    r1 * r2 * (/ r1) rnz == r2.
Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: creal.

Lemma Rinv_mult_simpl :
  forall r1 r2 r3 (r1nz : r1 # 0) (r2nz : r2 # 0),
    r1 * (/ r2) r2nz * (r3 * (/ r1) r1nz) == r3 * (/ r2) r2nz.

Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0),
    x == y
    -> (/ x) rxnz == (/ y) rynz.

Order and inverse


Lemma Rinv_lt_0_compat : forall r (rneg : r < 0), (/ r) (inl rneg) < 0.
Hint Resolve Rinv_lt_0_compat: creal.

Miscellaneous

Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1.
Hint Resolve Rle_lt_0_plus_1: creal.

Lemma Rlt_plus_1 : forall r, r < r + 1.
Hint Resolve Rlt_plus_1: creal.

Lemma tech_Rgt_minus : forall r1 r2, 0 < r2 -> r1 > r1 - r2.

Injection from N to R

Lemma S_INR : forall n:nat, INR (S n) == INR n + 1.

Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.

Lemma S_O_plus_INR : forall n:nat, INR (1 + n) == INR 1 + INR n.

Lemma plus_INR : forall n m:nat, INR (n + m) == INR n + INR m.

Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) == INR n - INR m.

Lemma mult_INR : forall n m:nat, INR (n * m) == INR n * INR m.

Lemma INR_IPR : forall p, INR (Pos.to_nat p) == IPR p.

Fixpoint pow (r:R) (n:nat) : R :=
  match n with
    | O => 1
    | S n => r * (pow r n)
  end.

Lemma Rpow_eq_compat : forall (x y : R) (n : nat),
    x == y -> pow x n == pow y n.

Lemma pow_INR (m n: nat) : INR (m ^ n) == pow (INR m) n.

Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n.
Hint Resolve lt_0_INR: creal.

Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n.
Hint Resolve lt_1_INR: creal.

Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (Pos.to_nat p).
Hint Resolve pos_INR_nat_of_P: creal.

Lemma pos_INR : forall n:nat, 0 <= INR n.
Hint Resolve pos_INR: creal.

Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
Hint Resolve INR_lt: creal.

Lemma le_INR : forall n m:nat, (n <= m)%nat -> INR n <= INR m.
Hint Resolve le_INR: creal.

Lemma INR_not_0 : forall n:nat, INR n <> 0 -> n <> 0%nat.
Hint Immediate INR_not_0: creal.

Lemma not_0_INR : forall n:nat, n <> 0%nat -> 0 < INR n.
Hint Resolve not_0_INR: creal.

Lemma not_INR : forall n m:nat, n <> m -> INR n # INR m.
Hint Resolve not_INR: creal.

Lemma INR_eq : forall n m:nat, INR n == INR m -> n = m.
Hint Resolve INR_eq: creal.

Lemma INR_le : forall n m:nat, INR n <= INR m -> (n <= m)%nat.
Hint Resolve INR_le: creal.

Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n # 1.
Hint Resolve not_1_INR: creal.

Injection from Z to R


Lemma IPR_pos : forall p:positive, 0 < IPR p.

Lemma IPR_double : forall p:positive, IPR (2*p) == 2 * IPR p.

Lemma INR_IZR_INZ : forall n:nat, INR n == IZR (Z.of_nat n).

Lemma plus_IZR_NEG_POS :
  forall p q:positive, IZR (Zpos p + Zneg q) == IZR (Zpos p) + IZR (Zneg q).

Lemma plus_IPR : forall n m:positive, IPR (n + m) == IPR n + IPR m.

Lemma plus_IZR : forall n m:Z, IZR (n + m) == IZR n + IZR m.

Lemma mult_IPR : forall n m:positive, IPR (n * m) == IPR n * IPR m.

Lemma mult_IZR : forall n m:Z, IZR (n * m) == IZR n * IZR m.

Lemma pow_IZR : forall z n, pow (IZR z) n == IZR (Z.pow z (Z.of_nat n)).

Lemma succ_IZR : forall n:Z, IZR (Z.succ n) == IZR n + 1.

Lemma opp_IZR : forall n:Z, IZR (- n) == - IZR n.

Definition Ropp_Ropp_IZR := opp_IZR.

Lemma minus_IZR : forall n m:Z, IZR (n - m) == IZR n - IZR m.

Lemma Z_R_minus : forall n m:Z, IZR n - IZR m == IZR (n - m).

Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.

Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.

Lemma eq_IZR_R0 : forall n:Z, IZR n == 0 -> n = 0%Z.

Lemma eq_IZR : forall n m:Z, IZR n == IZR m -> n = m.

Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.

Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n # 0.

Lemma le_0_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z.

Lemma le_IZR : forall n m:Z, IZR n <= IZR m -> (n <= m)%Z.

Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z.

Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m.

Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.

Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 # IZR z2.

Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : creal.
Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : creal.
Hint Extern 0 (IZR _ < IZR _) => apply IZR_lt, eq_refl : creal.
Hint Extern 0 (IZR _ > IZR _) => apply IZR_lt, eq_refl : creal.
Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : creal.

Lemma one_IZR_lt1 : forall n:Z, -(1) < IZR n < 1 -> n = 0%Z.

Lemma one_IZR_r_R1 :
  forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m.

Lemma single_z_r_R1 :
  forall r (n m:Z),
    r < IZR n -> IZR n <= r + 1 -> r < IZR m -> IZR m <= r + 1 -> n = m.

Lemma tech_single_z_r_R1 :
  forall r (n:Z),
    r < IZR n ->
    IZR n <= r + 1 ->
    { s : Z & prod (s <> n) (r < IZR s <= r + 1) } -> False.

Lemma Rmult_le_compat_l_half : forall r r1 r2,
    0 < r -> r1 <= r2 -> r * r1 <= r * r2.

Lemma INR_gen_phiZ : forall (n : nat),
    gen_phiZ 0 1 Rplus Rmult Ropp (Z.of_nat n) == INR n.

Definition Rup_nat (x : R)
  : { n : nat & x < INR n }.

Fixpoint Rarchimedean_ind (x:R) (n : Z) (p:nat) { struct p }
  : (x < IZR n < x + 2 + (INR p))
    -> { n:Z & x < IZR n < x+2 }.

Lemma Rarchimedean (x:R) : { n : Z & x < IZR n < x + 2 }.

Lemma Rmult_le_0_compat : forall a b,
    0 <= a -> 0 <= b -> 0 <= a * b.

Lemma Rmult_le_compat_l : forall r r1 r2,
    0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
Hint Resolve Rmult_le_compat_l: creal.

Lemma Rmult_le_compat_r : forall r r1 r2,
    0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
Hint Resolve Rmult_le_compat_r: creal.

Lemma Rmult_le_0_lt_compat :
  forall r1 r2 r3 r4,
    0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.

Lemma Rmult_le_compat_neg_l :
  forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1.
Hint Resolve Rmult_le_compat_neg_l: creal.

Lemma Rmult_le_ge_compat_neg_l :
  forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r1 >= r * r2.
Hint Resolve Rmult_le_ge_compat_neg_l: creal.

Lemma Rmult_ge_compat_l :
  forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2.

Lemma Rmult_ge_compat_r :
  forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r.

Lemma Rmult_le_compat :
  forall r1 r2 r3 r4,
    0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
Hint Resolve Rmult_le_compat: creal.

Lemma Rmult_ge_compat :
  forall r1 r2 r3 r4,
    r2 >= 0 -> r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4.

Lemma mult_IPR_IZR : forall (n:positive) (m:Z), IZR (Z.pos n * m) == IPR n * IZR m.

Definition IQR (q:Q) : R :=
  match q with
  | Qmake a b => IZR a * (/ (IPR b)) (inr (IPR_pos b))
  end.

Lemma plus_IQR : forall n m:Q, IQR (n + m) == IQR n + IQR m.

Lemma IQR_pos : forall q:Q, Qlt 0 q -> 0 < IQR q.

Lemma opp_IQR : forall q:Q, IQR (- q) == - IQR q.

Lemma lt_IQR : forall n m:Q, IQR n < IQR m -> (n < m)%Q.

Lemma IQR_lt : forall n m:Q, Qlt n m -> IQR n < IQR m.

Lemma IQR_nonneg : forall q:Q, Qle 0 q -> 0 <= (IQR q).

Lemma IQR_le : forall n m:Q, Qle n m -> IQR n <= IQR m.

Add Parametric Morphism : IQR
    with signature Qeq ==> Req
      as IQR_morph.

Instance IQR_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful Qeq Req) IQR.

Fixpoint Rfloor_pos (a : R) (n : nat) { struct n }
  : 0 < a
    -> a < INR n
    -> { p : nat & INR p < a < INR p + 2 }.

Definition Rfloor (a : R)
  : { p : Z & IZR p < a < IZR p + 2 }.

Definition RQ_dense (a b : R)
  : a < b -> { q : Q & a < IQR q < b }.

Definition RQ_limit : forall (x : R) (n:nat),
    { q:Q & x < IQR q < x + IQR (1 # Pos.of_nat n) }.

Lemma Rlt_lpo_dec : forall x y : R,
    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
                    -> {n | ~P n} + {forall n, P n})
    -> (x < y) + (y <= x).

Lemma Rlt_lpo_floor : forall x : R,
    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
                    -> {n | ~P n} + {forall n, P n})
    -> { p : Z & IZR p <= x < IZR p + 1 }.

Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.

Lemma Rinv_le_contravar :
  forall x y (xpos : 0 < x) (ynz : y # 0),
    x <= y -> (/ y) ynz <= (/ x) (inr xpos).

Lemma Rle_Rinv : forall x y (xpos : 0 < x) (ypos : 0 < y),
    x <= y -> (/ y) (inr ypos) <= (/ x) (inr xpos).

Lemma Ropp_div : forall x y (ynz : y # 0),
    -x * (/y) ynz == - (x * (/ y) ynz).

Lemma double : forall r1, 2 * r1 == r1 + r1.

Lemma Rlt_0_2 : 0 < 2.

Lemma double_var : forall r1, r1 == r1 * (/ 2) (inr Rlt_0_2)
                                    + r1 * (/ 2) (inr Rlt_0_2).

Lemma R_rm : ring_morph
  0 1 Rplus Rmult Rminus Ropp Req
  0%Z 1%Z Zplus Zmult Zminus Z.opp Zeq_bool IZR.

Lemma Zeq_bool_IZR x y :
  IZR x == IZR y -> Zeq_bool x y = true.

Other rules about < and <=


Lemma Rmult_ge_0_gt_0_lt_compat :
  forall r1 r2 r3 r4,
    r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.

Lemma le_epsilon :
  forall r1 r2, (forall eps, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2.

Lemma Rdiv_lt_0_compat : forall a b (bpos : 0 < b),
    0 < a -> 0 < a * (/b) (inr bpos).

Lemma Rdiv_plus_distr : forall a b c (cnz : c # 0),
    (a + b)* (/c) cnz == a* (/c) cnz + b* (/c) cnz.

Lemma Rdiv_minus_distr : forall a b c (cnz : c # 0),
    (a - b)* (/c) cnz == a* (/c) cnz - b* (/c) cnz.

Definitions of new types


Record nonnegreal : Type := mknonnegreal
  {nonneg :> R; cond_nonneg : 0 <= nonneg}.

Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.

Record nonposreal : Type := mknonposreal
  {nonpos :> R; cond_nonpos : nonpos <= 0}.

Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}.

Record nonzeroreal : Type := mknonzeroreal
  {nonzero :> R; cond_nonzero : nonzero <> 0}.