Library Coq.Reals.RIneq


Basic lemmas for the classical real numbers

This file provides several hundred basic lemmas about foundamental operations on R:
  • addition denoted by Rplus (notation: infix +), opposite denoted by Ropp (notation: unary prefix -) and subtraction denoted by Rminus (notation: infix -);
  • multiplication denoted by Rmult (notation: infix *), inverse denoted by Rinv (notation: prefix /), division denoted by Rdiv (notation: infix /) and square denoted by Rsqr (notation: suffix ²)
  • orders <, >, <= and >=
  • injective morphisms:
    • INR : nat -> R
    • IPR : positive -> R
    • IZR : Z -> R
All those lemmas are proved using a set of 17 "primitive" lemmas in Raxioms.v (plus the convenient choice that the inverse of 0 is 0 in Rdefinitions.v). These "primitive" lemmas are:
  • Rplus_comm, Rplus_assoc, Rplus_0_l, Rplus_opp_l
  • Rmult_comm, Rmult_assoc, Rmult_1_l, Rinv_l
  • Rmult_plus_distr_l, R1_neq_R0
  • Rlt_trans, Rlt_asym, Rplus_lt_compat_l, Rmult_lt_compat_l
  • total_order_T
  • completeness, archimed
This makes this file independent of the actual construction of the real numbers, since these 17 axioms characterize, up to isomorphism, the ordered field of real numbers.

Require Import RelationClasses.
Require Export Raxioms.
Require Import Rpow_def.
Require Import ZArith.
Require Export ZArithRing.
Require Export RealField.

Local Open Scope Z_scope.
Local Open Scope R_scope.

Relation between orders and equality

Reflexivity of the large orders

Lemma Rle_refl : forall r, r <= r.
#[global]
Hint Immediate Rle_refl: rorders.

#[export] Instance Rle_Reflexive : Reflexive Rle | 10 := Rle_refl.

Lemma Rge_refl : forall r, r >= r.
#[global]
Hint Immediate Rge_refl: rorders.

#[export] Instance Rge_Reflexive : Reflexive Rge | 10 := Rge_refl.

Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2.
#[global]
Hint Immediate Req_le: real.

Lemma Req_ge : forall r1 r2, r1 = r2 -> r1 >= r2.
#[global]
Hint Immediate Req_ge: real.

Irreflexivity of the strict orders

Lemma Rlt_irrefl : forall r, ~ r < r.
#[global]
Hint Resolve Rlt_irrefl: real.

#[export] Instance Rlt_Irreflexive : Irreflexive Rlt | 10 := Rlt_irrefl.

Lemma Rgt_irrefl : forall r, ~ r > r.

#[export] Instance Rgt_Irreflexive : Irreflexive Rgt | 10 := Rgt_irrefl.

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.
#[global]
Hint Resolve Rlt_dichotomy_converse: real.

Reasoning by case on equality and order

Lemma Rtotal_order : forall r1 r2, r1 < r2 \/ r1 = r2 \/ r1 > r2.

Lemma Req_dec : forall r1 r2:R, r1 = r2 \/ r1 <> r2.
#[global]
Hint Resolve Req_dec: real.

Lemma Rdichotomy : forall r1 r2, r1 <> r2 -> r1 < r2 \/ r1 > r2.

Strong decidable equality


Lemma Req_dec_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.

Relating <, >, <= and >=

Relating strict and large orders


Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
#[global]
Hint Resolve Rlt_le: real.

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

Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1.
#[global]
Hint Immediate Rle_ge: real.
#[global]
Hint Resolve Rle_ge: rorders.

Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1.
#[global]
Hint Resolve Rge_le: real.
#[global]
Hint Immediate Rge_le: rorders.

Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1.
#[global]
Hint Resolve Rlt_gt: rorders.

Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1.
#[global]
Hint Immediate Rgt_lt: rorders.

Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1.
#[global]
Hint Immediate Rnot_le_lt: real.

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

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

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

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

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

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

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

Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
#[global]
Hint Immediate Rlt_not_le: real.

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

Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2.
#[global]
Hint Immediate Rlt_not_ge: real.

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

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

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

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

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

Lemma Req_le_sym : forall r1 r2, r2 = r1 -> r1 <= r2.
#[global]
Hint Immediate Req_le_sym: real.

Lemma Req_ge_sym : forall r1 r2, r2 = r1 -> r1 >= r2.
#[global]
Hint Immediate Req_ge_sym: real.

Asymmetry

Remark: Rlt_asym is in Raxioms.v

#[export] Instance Rlt_Asymmetric : Asymmetric Rlt | 10 := Rlt_asym.

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

#[export] Instance Rgt_Asymmetric : Asymmetric Rgt | 10 := Rgt_asym.

Antisymmetry


Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2.
#[global]
Hint Resolve Rle_antisym: real.

#[export] Instance Rle_Antisymmetric : Antisymmetric R eq Rle | 10 := Rle_antisym.

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

#[export] Instance Rge_Antisymmetric : Antisymmetric R eq Rge | 10 := Rge_antisym.

Lemma Rle_le_eq : forall r1 r2, r1 <= r2 /\ r2 <= r1 <-> r1 = r2.

Lemma Rge_ge_eq : forall r1 r2, r1 >= r2 /\ r2 >= r1 <-> r1 = r2.

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

Remark: Rlt_trans is in Raxioms
#[export] Instance Rlt_Transitive : Transitive Rlt | 10 := Rlt_trans.

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

#[export] Instance Rle_Transitive : Transitive Rle | 10 := Rle_trans.

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

#[export] Instance Rge_Transitive : Transitive Rge | 10 := Rge_trans.

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

#[export] Instance Rgt_Transitive : Transitive Rgt | 10 := Rgt_trans.

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.

(Classical) decidability with sumbool types


Lemma Rlt_dec : forall r1 r2, {r1 < r2} + {~ r1 < r2}.

Lemma Rle_dec : forall r1 r2, {r1 <= r2} + {~ r1 <= r2}.

Lemma Rgt_dec : forall r1 r2, {r1 > r2} + {~ r1 > r2}.

Lemma Rge_dec : forall r1 r2, {r1 >= r2} + {~ r1 >= r2}.

Lemma Rlt_le_dec : forall r1 r2, {r1 < r2} + {r2 <= r1}.

Lemma Rlt_ge_dec : forall r1 r2, {r1 < r2} + {r1 >= r2}.

Lemma Rgt_ge_dec : forall r1 r2, {r1 > r2} + {r2 >= r1}.

Lemma Rgt_le_dec : forall r1 r2, {r1 > r2} + {r1 <= r2}.

Lemma Rle_lt_dec : forall r1 r2, {r1 <= r2} + {r2 < r1}.

Lemma Rle_gt_dec : forall r1 r2, {r1 <= r2} + {r1 > r2}.

Lemma Rge_gt_dec : forall r1 r2, {r1 >= r2} + {r2 > r1}.

Lemma Rge_lt_dec : forall r1 r2, {r1 >= r2} + {r1 < r2}.

Lemma Rle_lt_or_eq_dec : forall r1 r2, r1 <= r2 -> {r1 < r2} + {r1 = r2}.

Lemma Rge_gt_or_eq_dec : forall r1 r2, r1 >= r2 -> {r1 > r2} + {r1 = r2}.

Same theorems with disjunctions instead of sumbools


Lemma Private_sumbool_to_or {A B : Prop} : {A} + {B} -> A \/ B.

Lemma Rlt_or_not_lt : forall r1 r2, r1 < r2 \/ ~(r1 < r2).

Lemma Rle_or_not_le : forall r1 r2, r1 <= r2 \/ ~(r1 <= r2).

Lemma Rgt_or_not_gt : forall r1 r2, r1 > r2 \/ ~(r1 > r2).

Lemma Rge_or_not_ge : forall r1 r2, r1 >= r2 \/ ~(r1 >= r2).

Lemma Rlt_or_le : forall r1 r2, r1 < r2 \/ r2 <= r1.

Lemma Rgt_or_ge : forall r1 r2, r1 > r2 \/ r2 >= r1.

Lemma Rle_or_lt : forall r1 r2, r1 <= r2 \/ r2 < r1.

Lemma Rge_or_gt : forall r1 r2, r1 >= r2 \/ r2 > r1.

Lemma Rlt_or_ge : forall r1 r2, r1 < r2 \/ r1 >= r2.

Lemma Rgt_or_le : forall r1 r2, r1 > r2 \/ r1 <= r2.

Lemma Rle_or_gt : forall r1 r2, r1 <= r2 \/ r1 > r2.

Lemma Rge_or_lt : forall r1 r2, r1 >= r2 \/ r1 < r2.

Lemma Rle_lt_or_eq : forall r1 r2, r1 <= r2 -> r1 < r2 \/ r1 = r2.

Lemma Rge_gt_or_eq : forall r1 r2, r1 >= r2 -> r1 > r2 \/ r1 = r2.

Addition


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.

Remark: the following primitive lemmas are in Raxioms.v
  • Rplus_0_l;
  • Rplus_comm;
  • Rplus_opp_r and
  • Rplus_assoc

Lemma Rplus_0_r : forall r, r + 0 = r.
#[global]
Hint Resolve Rplus_0_r: real.

Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r.
#[global]
Hint Resolve Rplus_ne: real.

Lemma Rplus_opp_l : forall r, - r + r = 0.
#[global]
Hint Resolve Rplus_opp_l: real.

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

Definition f_equal_R := (f_equal (A:=R)).
#[global]
Hint Resolve f_equal_R : real.

Lemma Rplus_eq_reg_l : forall r r1 r2, r + r1 = r + r2 -> r1 = r2.
#[global]
Hint Resolve Rplus_eq_reg_l: real.

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.

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

Opposite


Lemma Ropp_eq_compat : forall r1 r2, r1 = r2 -> - r1 = - r2.
#[global]
Hint Resolve Ropp_eq_compat: real.

Lemma Ropp_0 : -0 = 0.
#[global]
Hint Resolve Ropp_0: real.

Lemma Ropp_eq_0_compat : forall r, r = 0 -> - r = 0.
#[global]
Hint Resolve Ropp_eq_0_compat: real.

Lemma Ropp_involutive : forall r, - - r = r.
#[global]
Hint Resolve Ropp_involutive: real.

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

Lemma Ropp_neq_0_compat : forall r, r <> 0 -> - r <> 0.
#[global]
Hint Resolve Ropp_neq_0_compat: real.

Lemma Ropp_plus_distr : forall r1 r2, - (r1 + r2) = - r1 + - r2.
#[global]
Hint Resolve Ropp_plus_distr: real.

Multiplication


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.

Remark: the following primitive lemmas are in Raxioms.v
  • Rmult_comm;
  • Rinv_l;
  • Rmult_assoc;
  • Rmult_1_l and
  • Rmult_plus_distr_l

Lemma Rinv_r : forall r, r <> 0 -> r * / r = 1.
#[global]
Hint Resolve Rinv_r: real.

Lemma Rinv_l_sym : forall r, r <> 0 -> 1 = / r * r.
#[global]
Hint Resolve Rinv_l_sym: real.

Lemma Rinv_r_sym : forall r, r <> 0 -> 1 = r * / r.
#[global]
Hint Resolve Rinv_r_sym: real.

Definition Rmult_inv_r := Rinv_r.
Definition Rmult_inv_l := Rinv_l.

Lemma Rmult_1_r : forall r, r * 1 = r.
#[global]
Hint Resolve Rmult_1_r: real.

Lemma Rmult_ne : forall r, r * 1 = r /\ 1 * r = r.
#[global]
Hint Resolve Rmult_ne: real.

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_plus_distr_r :
  forall r1 r2 r3, (r1 + r2) * r3 = r1 * r3 + r2 * r3.

Lemma Rmult_0_r : forall r, r * 0 = 0.
#[global]
Hint Resolve Rmult_0_r: real.

Lemma Rmult_0_l : forall r, 0 * r = 0.
#[global]
Hint Resolve Rmult_0_l: real.

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

Lemma Rmult_eq_0_compat : forall r1 r2, r1 = 0 \/ r2 = 0 -> r1 * r2 = 0.
#[global]
Hint Resolve Rmult_eq_0_compat: real.

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_neq_0_reg : forall r1 r2, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0.

Lemma Rmult_integral_contrapositive :
  forall r1 r2, r1 <> 0 /\ r2 <> 0 -> r1 * r2 <> 0.
#[global]
Hint Resolve Rmult_integral_contrapositive: real.

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

Opposite and multiplication


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

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

Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2).
#[global]
Hint Resolve Ropp_mult_distr_l_reverse: real.

Lemma Rmult_opp_opp : forall r1 r2, - r1 * - r2 = r1 * r2.
#[global]
Hint Resolve Rmult_opp_opp: real.

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

Subtraction


Lemma Rminus_def : forall r1 r2, r1 - r2 = r1 + - r2.

Lemma Rminus_eq_compat_l : forall r r1 r2, r1 = r2 -> r - r1 = r - r2.

Lemma Rminus_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 - r = r2 - r.

Lemma Rminus_eq_reg_l : forall r r1 r2, r - r1 = r - r2 -> r1 = r2.

Lemma Rminus_eq_reg_r : forall r r1 r2, r1 - r = r2 - r -> r1 = r2.

Lemma Rminus_0_r : forall r, r - 0 = r.
#[global]
Hint Resolve Rminus_0_r: real.

Lemma Rminus_0_l : forall r, 0 - r = - r.
#[global]
Hint Resolve Rminus_0_l: real.

Lemma Ropp_minus_distr : forall r1 r2, - (r1 - r2) = r2 - r1.
#[global]
Hint Resolve Ropp_minus_distr: real.

Lemma Rminus_diag_eq : forall r1 r2, r1 = r2 -> r1 - r2 = 0.
#[global]
Hint Resolve Rminus_diag_eq: real.

Lemma Rminus_diag : forall r, r - r = 0.

Lemma Rminus_diag_uniq : forall r1 r2, r1 - r2 = 0 -> r1 = r2.
#[global]
Hint Immediate Rminus_diag_uniq: real.

Lemma Rminus_diag_uniq_sym : forall r1 r2, r2 - r1 = 0 -> r1 = r2.
#[global]
Hint Immediate Rminus_diag_uniq_sym: real.

Lemma Rplus_minus : forall r1 r2, r1 + (r2 - r1) = r2.
#[global]
Hint Resolve Rplus_minus: real.

Lemma Rminus_eq_contra : forall r1 r2, r1 <> r2 -> r1 - r2 <> 0.
#[global]
Hint Resolve Rminus_eq_contra: real.

Lemma Rminus_not_eq : forall r1 r2, r1 - r2 <> 0 -> r1 <> r2.
#[global]
Hint Resolve Rminus_not_eq: real.

Lemma Rminus_not_eq_right : forall r1 r2, r2 - r1 <> 0 -> r1 <> r2.
#[global]
Hint Resolve Rminus_not_eq_right: real.

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

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

Lemma Rplus_minus_r : forall r1 r2, r1 + r2 - r2 = r1.

Lemma Rplus_minus_l : forall r1 r2, r1 + r2 - r1 = r2.

Lemma Rplus_minus_assoc : forall r1 r2 r3, r1 + (r2 - r3) = (r1 + r2) - r3.

Lemma Rplus_minus_swap : forall r1 r2 r3, (r1 + r2) - r3 = (r1 - r3) + r2.

Lemma Rminus_plus_distr : forall r1 r2 r3, r1 - (r2 + r3) = (r1 - r2) - r3.

Lemma Rminus_plus_r_r : forall r r1 r2, (r1 + r) - (r2 + r) = r1 - r2.

Lemma Rminus_plus_l_r : forall r r1 r2, (r + r1) - (r2 + r) = r1 - r2.

Lemma Rminus_plus_r_l : forall r r1 r2, (r1 + r) - (r + r2) = r1 - r2.

Lemma Rminus_plus_l_l : forall r r1 r2, (r + r1) - (r + r2) = r1 - r2.

Inverse


Lemma Rinv_0 : / 0 = 0.

Lemma Rmult_inv_r_uniq :
  forall r1 r2, r1 <> 0 -> r1 * r2 = 1 -> r2 = / r1.

Lemma Rinv_eq_compat : forall r1 r2, r1 = r2 -> / r1 = / r2.

Lemma Rinv_1 : / 1 = 1.
#[global]
Hint Resolve Rinv_1: real.

Lemma Rinv_neq_0_compat : forall r, r <> 0 -> / r <> 0.
#[global]
Hint Resolve Rinv_neq_0_compat: real.

Lemma Rinv_inv r : / / r = r.
#[global]
Hint Resolve Rinv_inv: real.

Lemma Rinv_eq_reg : forall r1 r2, / r1 = / r2 -> r1 = r2.

Lemma Rinv_mult r1 r2 : / (r1 * r2) = / r1 * / r2.

Lemma Rinv_opp r : / - r = - / r.

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

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

Lemma Rmult_inv_r_id_m : forall r1 r2, r1 <> 0 -> r1 * r2 * / r1 = r2.
#[global]
Hint Resolve Rmult_inv_m_id_r Rmult_inv_r_id_l Rmult_inv_r_id_m: real.

Square function


Definition Rsqr r : R := r * r.
Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope.

Lemma Rsqr_def : forall r, r² = r * r.

Lemma Rsqr_0 : Rsqr 0 = 0.

Lemma Rsqr_0_uniq : forall r, Rsqr r = 0 -> r = 0.

Order and addition

Compatibility

Remark: Rplus_lt_compat_l is in Raxioms.v

Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2.
#[global]
Hint Resolve Rplus_gt_compat_l: real.

Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r.
#[global]
Hint Resolve Rplus_lt_compat_r: real.

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

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.
#[global]
Hint Resolve Rplus_ge_compat_l: real.

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

#[global]
Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real.

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.
#[global]
Hint Immediate Rplus_lt_compat: real.

Lemma Rplus_le_compat :
  forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
#[global]
Hint Immediate Rplus_le_compat: real.

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.
#[global]
Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: real.

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 Rplus_eq_0_l :
  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0.

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

Cancellation


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

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

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_gt_reg_r : forall r r1 r2, r1 + r > r2 + r -> r1 > r2.

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

Lemma Rplus_ge_reg_r : forall r r1 r2, r1 + r >= r2 + r -> 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_le_lt_0_neq_0 : forall r1 r2, 0 <= r1 -> 0 < r2 -> r1 + r2 <> 0.
#[global]
Hint Immediate Rplus_le_lt_0_neq_0: real.

Comparison of addition with left operand


Lemma Rplus_pos_gt : forall r1 r2, r2 > 0 -> r1 + r2 > r1.

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

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

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

Sign of addition


Lemma Rplus_pos_pos : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 + r2 > 0.

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

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

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

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

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

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

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

Order and opposite

Contravariant compatibility


Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
#[global]

Hint Resolve Ropp_gt_lt_contravar : core.

Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
#[global]
Hint Resolve Ropp_lt_gt_contravar: real.

Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2.
#[global]
Hint Resolve Ropp_lt_contravar: real.

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

Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2.
#[global]
Hint Resolve Ropp_le_ge_contravar: real.

Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
#[global]
Hint Resolve Ropp_ge_le_contravar: real.

Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2.
#[global]
Hint Resolve Ropp_le_contravar: real.

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

Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r.
#[global]
Hint Resolve Ropp_0_lt_gt_contravar: real.

Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r.
#[global]
Hint Resolve Ropp_0_gt_lt_contravar: real.

Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0.
#[global]
Hint Resolve Ropp_lt_gt_0_contravar: real.

Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0.
#[global]
Hint Resolve Ropp_gt_lt_0_contravar: real.

Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r.
#[global]
Hint Resolve Ropp_0_le_ge_contravar: real.

Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r.
#[global]
Hint Resolve Ropp_0_ge_le_contravar: real.

Cancellation


Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
#[global]
Hint Immediate Ropp_lt_cancel: real.

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

Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2.
#[global]
Hint Immediate Ropp_le_cancel: real.

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

Sign of opposite


Lemma Ropp_pos : forall r, r > 0 -> - r < 0.

Lemma Ropp_neg : forall r, r < 0 -> - r > 0.

Order and multiplication

Remark: Rmult_lt_compat_l is in Raxioms.v

Covariant compatibility


Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
#[global]

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_le_compat_l :
  forall r r1 r2, 0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
#[global]
Hint Resolve Rmult_le_compat_l: real.

Lemma Rmult_le_compat_r :
  forall r r1 r2, 0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
#[global]
Hint Resolve Rmult_le_compat_r: real.

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.
#[global]
Hint Resolve Rmult_le_compat: real.

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

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

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 Rmult_gt_0_lt_compat :
  forall r1 r2 r3 r4,
    r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.

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

Contravariant compatibility


Lemma Rmult_le_compat_neg_l :
  forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1.
#[global]
Hint Resolve Rmult_le_compat_neg_l: real.

Lemma Rmult_le_ge_compat_neg_l :
  forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r1 >= r * r2.
#[global]
Hint Resolve Rmult_le_ge_compat_neg_l: real.

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

Sign of multiplication


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.

Definition Rmult_pos_pos := Rmult_gt_0_compat.

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

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

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

Lemma Rmult_pos_cases :
  forall r1 r2, r1 * r2 > 0 -> (r1 > 0 /\ r2 > 0) \/ (r1 < 0 /\ r2 < 0).

Lemma Rmult_neg_cases :
  forall r1 r2, r1 * r2 < 0 -> (r1 > 0 /\ r2 < 0) \/ (r1 < 0 /\ r2 > 0).

Order and square function


Lemma Rle_0_sqr : forall r, 0 <= Rsqr r.

Lemma Rlt_0_sqr : forall r, r <> 0 -> 0 < Rsqr r.
#[global]
Hint Resolve Rle_0_sqr Rlt_0_sqr: real.

Lemma Rplus_sqr_eq_0 :
  forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0.

Zero is less than one


Lemma Rlt_0_1 : 0 < 1.
#[global]
Hint Resolve Rlt_0_1: real.

Lemma Rle_0_1 : 0 <= 1.

Sign of inverse


Lemma Rinv_0_lt_compat : forall r, 0 < r -> 0 < / r.
#[global]
Hint Resolve Rinv_0_lt_compat: real.

Lemma Rinv_lt_0_compat : forall r, r < 0 -> / r < 0.
#[global]
Hint Resolve Rinv_lt_0_compat: real.

Cancellation in inequalities of products


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 : R, 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_gt_reg_r : forall r r1 r2, r > 0 -> r1 * r > r2 * r -> 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 inverse


Lemma Rinv_0_lt_contravar : forall r1 r2, 0 < r1 -> r1 < r2 -> / r2 < / r1.
#[global]
Hint Resolve Rinv_0_lt_contravar: real.

Lemma Rinv_lt_0_contravar : forall r1 r2, r2 < 0 -> r1 < r2 -> / r2 < / r1.
#[global]
Hint Resolve Rinv_lt_0_contravar: real.

Lemma Rinv_1_lt_contravar : forall r1 r2, 1 <= r1 -> r1 < r2 -> / r2 < / r1.
#[global]
Hint Resolve Rinv_1_lt_contravar: real.

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

Lemma Rinv_le_contravar :
  forall x y, 0 < x -> x <= y -> / y <= / x.

Sign of inverse


Lemma Rinv_pos : forall r, r > 0 -> / r > 0.

Lemma Rinv_neg : forall r, r < 0 -> / r < 0.

Order and subtraction


Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0.
#[global]
Hint Resolve Rlt_minus: real.

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

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 Rlt_minus_0 : forall r1 r2, r1 - r2 < 0 <-> r1 < r2.

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

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

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

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

Division


Lemma Rdiv_def : forall r1 r2, r1 / r2 = r1 * / r2.

Lemma Rdiv_eq_compat_l : forall r r1 r2, r1 = r2 -> r / r1 = r / r2.

Lemma Rdiv_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 / r = r2 / r.

Lemma Rdiv_eq_reg_l : forall r r1 r2, r / r1 = r / r2 -> r <> 0 -> r1 = r2.

Lemma Rdiv_eq_reg_r : forall r r1 r2, r1 / r = r2 / r -> r <> 0 -> r1 = r2.

Lemma Rdiv_0_l : forall r, 0 / r = 0.

Lemma Rdiv_0_r : forall r, r / 0 = 0.

Lemma Rdiv_1_l : forall r, 1 / r = / r.

Lemma Rdiv_1_r : forall r, r / 1 = r.

Lemma Rdiv_diag : forall r, r <> 0 -> r / r = 1.

Lemma Rdiv_diag_eq : forall r1 r2, r2 <> 0 -> r1 = r2 -> r1 / r2 = 1.

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

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

Lemma Rmult_div_assoc : forall r1 r2 r3, r1 * (r2 / r3) = r1 * r2 / r3.

Lemma Rmult_div_swap : forall r1 r2 r3, r1 * r2 / r3 = r1 / r3 * r2.

Lemma Rdiv_diag_uniq : forall r1 r2, r1 / r2 = 1 -> r1 = r2.

Lemma Rdiv_mult_distr : forall r1 r2 r3, r1 / (r2 * r3) = r1 / r2 / r3.

Lemma Rdiv_mult_r_r :
  forall r r1 r2, r <> 0 -> (r1 * r) / (r2 * r) = r1 / r2.

Lemma Rdiv_mult_l_r :
  forall r r1 r2, r <> 0 -> (r * r1) / (r2 * r) = r1 / r2.

Lemma Rdiv_mult_l_l :
  forall r r1 r2, r <> 0 -> (r * r1) / (r * r2) = r1 / r2.

Lemma Rdiv_mult_r_l :
  forall r r1 r2, r <> 0 -> (r1 * r) / (r * r2) = r1 / r2.

Lemma Ropp_div_distr_l : forall r1 r2, - (r1 / r2) = - r1 / r2.

Lemma Ropp_div_distr_r : forall r1 r2, r1 / - r2 = - (r1 / r2).

Lemma Rdiv_plus_distr : forall a b c, (a + b) / c = a / c + b / c.

Lemma Rdiv_minus_distr : forall a b c, (a - b) / c = a / c - b / c.

Lemma Rinv_div x y : / (x / y) = y / x.

Lemma Rdiv_lt_0_compat : forall a b, 0 < a -> 0 < b -> 0 < a / b.

Lemma Rdiv_opp_l : forall r1 r2, - r1 / r2 = - (r1 / r2).

Lemma Rdiv_opp_r : forall x y, x / - y = - (x / y).

Sign of division


Lemma Rdiv_pos_pos : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 / r2 > 0.

Lemma Rdiv_pos_neg : forall r1 r2, r1 > 0 -> r2 < 0 -> r1 / r2 < 0.

Lemma Rdiv_neg_pos : forall r1 r2, r1 < 0 -> r2 > 0 -> r1 / r2 < 0.

Lemma Rdiv_neg_neg : forall r1 r2, r1 < 0 -> r2 < 0 -> r1 / r2 > 0.

Lemma Rdiv_pos_cases :
  forall r1 r2 : R, r1 / r2 > 0 -> r1 > 0 /\ r2 > 0 \/ r1 < 0 /\ r2 < 0.

Miscellaneous



Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1.
#[global]
Hint Resolve Rle_lt_0_plus_1: real.

Lemma Rlt_plus_1 : forall r, r < r + 1.
#[global]
Hint Resolve Rlt_plus_1: real.

Lemma Rlt_0_2 : 0 < 2.

Lemma Rplus_diag : forall r, r + r = 2 * r.

Lemma Rplus_half_diag : forall r, r / 2 + r / 2 = r.

Lemma Rlt_half_plus : forall r1 r2, r1 < r2 -> r1 < (r1 + r2) / 2 < r2.

Lemma Rle_half_plus : forall r1 r2, r1 <= r2 -> r1 <= (r1 + r2) / 2 <= r2.

Lemma Rexists_between : forall r1 r2, r1 < r2 -> exists r, r1 < r < r2.

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

Remark : a sigma-type version, called completeness is in Raxioms.v
Lemma upper_bound_thm :
  forall E : R -> Prop,
    bound E -> (exists x : R, E x) -> exists m : R, is_lub E m.

Injection from nat to R


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

Lemma INR_0 : INR 0 = 0.

Lemma INR_1 : INR 1 = 1.

Lemma plus_INR : forall n m, INR (n + m) = INR n + INR m.
#[global]
Hint Resolve plus_INR: real.

Lemma minus_INR : forall n m, (m <= n)%nat -> INR (n - m) = INR n - INR m.
#[global]
Hint Resolve minus_INR: real.

Lemma mult_INR : forall n m:nat, INR (n * m) = INR n * INR m.
#[global]
Hint Resolve mult_INR: real.

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

Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n.
#[global]
Hint Resolve lt_0_INR: real.

Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.
#[global]
Hint Resolve lt_INR: real.

Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n.
#[global]
Hint Resolve lt_1_INR: real.

Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (Pos.to_nat p).
#[global]
Hint Resolve pos_INR_nat_of_P: real.

Lemma pos_INR : forall n:nat, 0 <= INR n.
#[global]
Hint Resolve pos_INR: real.

Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
#[global]
Hint Resolve INR_lt: real.

Lemma le_INR : forall n m:nat, (n <= m)%nat -> INR n <= INR m.
#[global]
Hint Resolve le_INR: real.

Lemma INR_not_0 : forall n:nat, INR n <> 0 -> n <> 0%nat.
#[global]
Hint Immediate INR_not_0: real.

Lemma not_0_INR : forall n:nat, n <> 0%nat -> INR n <> 0.
#[global]
Hint Resolve not_0_INR: real.

Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m.
#[global]
Hint Resolve not_INR: real.

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

Lemma INR_le : forall n m:nat, INR n <= INR m -> (n <= m)%nat.
#[global]
Hint Resolve INR_le: real.

Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n <> 1.
#[global]
Hint Resolve not_1_INR: real.

Injection from positive to R


Lemma IPR_2_xH : IPR_2 xH = 2.

Lemma IPR_2_xO : forall p : positive, IPR_2 (p~0) = 2 * (IPR_2 p).

Lemma IPR_2_xI : forall p : positive, IPR_2 (p~1) = 2 * (IPR_2 p) + 2.

Lemma IPR_xH : IPR xH = 1.

Lemma IPR_IPR_2 : forall p : positive, 2 * IPR p = IPR_2 p.

Lemma IPR_xO : forall p : positive, IPR (p~0) = 2 * IPR p.

Lemma IPR_xI : forall p : positive, IPR (p~1) = 2 * IPR p + 1.

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

Lemma succ_IPR : forall p, IPR (Pos.succ p) = IPR 1 + IPR p.

Lemma plus_IPR : forall p q, IPR (p + q) = IPR p + IPR q.

Lemma minus_IPR : forall p q, (q < p)%positive -> IPR (p - q) = IPR p - IPR q.

Lemma mult_IPR : forall p q:positive, IPR (p * q) = IPR p * IPR q.

Lemma pow_IPR (q p: positive) : IPR (q ^ p) = pow (IPR q) (Pos.to_nat p).

Lemma IPR_ge_1 : forall p:positive, 1 <= IPR p.

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

Lemma lt_IPR : forall p q:positive, (p < q)%positive -> IPR p < IPR q.

Lemma lt_1_IPR : forall p:positive, (1 < p)%positive -> 1 < IPR p.

Lemma IPR_lt : forall p q:positive, IPR p < IPR q -> (p < q)%positive.

Lemma le_IPR : forall p q:positive, (p <= q)%positive -> IPR p <= IPR q.

Lemma IPR_not_1 : forall p:positive, IPR p <> 1 -> p <> 1%positive.

Lemma not_1_IPR : forall p:positive, p <> 1%positive -> IPR p <> 1.

Lemma not_IPR : forall p q:positive, p <> q -> IPR p <> IPR q.

Lemma IPR_eq : forall p q:positive, IPR p = IPR q -> p = q.

Lemma IPR_le : forall p q:positive, IPR p <= IPR q -> (p <= q)%positive.

Injection from Z to R

Lemma IZN : forall n:Z, (0 <= n)%Z -> exists m : nat, n = Z.of_nat m.

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

Lemma IZR_NEG : forall p, IZR (Zneg p) = Ropp (IZR (Zpos p)).

The three following lemmas map the default form of numerical constants to their representation in terms of the axioms of R. This can be a useful intermediate representation for reifying to another axiomatics of the reals. It is however generally more convenient to keep constants represented under an IZR z form when working within R.

Lemma IZR_POS_xO : forall p, IZR (Zpos (p~0)) = 2 * (IZR (Zpos p)).

Lemma IZR_POS_xI : forall p, IZR (Zpos (xI p)) = 1 + 2 * IZR (Zpos p).

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

Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR 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 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_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.

Lemma eq_IZR_contrapositive : forall n m:Z, n <> m -> IZR n <> IZR m.

#[global]
Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : real.
#[global]
Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : real.
#[global]
Hint Extern 0 (IZR _ < IZR _) => apply IZR_lt, eq_refl : real.
#[global]
Hint Extern 0 (IZR _ > IZR _) => apply IZR_lt, eq_refl : real.
#[global]
Hint Extern 0 (IZR _ <> IZR _) => apply eq_IZR_contrapositive, Zeq_bool_neq, eq_refl : real.

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 INR_unbounded : forall A, exists n, INR n > A.

Lemma INR_archimed :
  forall eps A : R, eps > 0 -> exists n : nat, (INR n) * eps > A.

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

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

Add Field RField : Rfield
  (completeness Zeq_bool_IZR, morphism R_rm, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]).

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

A few common instances


Lemma pos_half_prf : 0 < / 2.

Definition posreal_one := mkposreal (1) (Rlt_0_1).
Definition posreal_half := mkposreal (/ 2) pos_half_prf.

Compatibility


Notation prod_neq_R0 := Rmult_integral_contrapositive_currified (only parsing).
Notation minus_Rgt := Rminus_gt (only parsing).
Notation minus_Rge := Rminus_ge (only parsing).
Notation plus_le_is_le := Rplus_le_reg_pos_r (only parsing).
Notation plus_lt_is_lt := Rplus_lt_reg_pos_r (only parsing).
Notation INR_lt_1 := lt_1_INR (only parsing).
Notation lt_INR_0 := lt_0_INR (only parsing).
Notation not_nm_INR := not_INR (only parsing).
Notation INR_pos := pos_INR_nat_of_P (only parsing).
Notation not_INR_O := INR_not_0 (only parsing).
Notation not_O_INR := not_0_INR (only parsing).
Notation not_O_IZR := not_0_IZR (only parsing).
Notation le_O_IZR := le_0_IZR (only parsing).
Notation lt_O_IZR := lt_0_IZR (only parsing).

Notation tech_Rplus := Rplus_le_lt_0_neq_0 (only parsing).
Notation tech_Rgt_minus := Rgt_minus_pos (only parsing).
Notation le_epsilon := Rle_plus_epsilon (only parsing).
Notation completeness_weak := upper_bound_thm (only parsing).
Notation Req_EM_T := Req_dec_T (only parsing).
Notation Rinv_r_simpl_r := Rmult_inv_m_id_r (only parsing).
Notation Rinv_r_simpl_l := Rmult_inv_r_id_l (only parsing).
Notation Rinv_r_simpl_m := Rmult_inv_r_id_m (only parsing).
Notation Rplus_eq_R0 := Rplus_eq_0 (only parsing).

Lemma Rinv_involutive_depr : forall r, r <> 0 -> / / r = r.
#[deprecated(since="8.16",note="Use Rinv_inv.")]
Notation Rinv_involutive := Rinv_involutive_depr (only parsing).

Lemma Rinv_mult_distr_depr :
  forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2.
#[deprecated(since="8.16",note="Use Rinv_mult.")]
Notation Rinv_mult_distr := Rinv_mult_distr_depr (only parsing).

Lemma Ropp_inv_permute_depr : forall r, r <> 0 -> - / r = / - r.
#[deprecated(since="8.16",note="Use Rinv_opp.")]
Notation Ropp_inv_permute := Ropp_inv_permute_depr (only parsing).

Lemma Ropp_div_den_depr : forall x y, y <> 0 -> x / - y = - (x / y).
#[deprecated(since="8.16",note="Use Rdiv_opp_r.")]
Notation Ropp_div_den := Ropp_div_den_depr (only parsing).

Lemma inser_trans_R_depr :
  forall r1 r2 r3 r4, r1 <= r2 < r3 -> {r1 <= r2 < r4} + {r4 <= r2 < r3}.
#[deprecated(since="8.19")]
Notation inser_trans_R := inser_trans_R_depr (only parsing).

Lemma Ropp_minus_distr'_depr : forall r1 r2, - (r2 - r1) = r1 - r2.
#[deprecated(since="8.19",note="Use Ropp_minus_distr instead.")]
Notation Ropp_minus_distr' := (fun r1 r2 => (Ropp_minus_distr r2 r1)) (only parsing).

#[deprecated(since="8.19",note="Use Rminus_diag instead.")]
Notation Rminus_eq_0 := (fun x => Rminus_diag x) (only parsing).

Lemma sum_inequa_Rle_lt_depr :
  forall a x b c y d:R,
    a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.
#[deprecated(since="8.19")]
Notation sum_inequa_Rle_lt := sum_inequa_Rle_lt_depr (only parsing).

Lemma Rle_Rinv_depr : forall x y:R, 0 < x -> 0 < y -> x <= y -> / y <= / x.
#[deprecated(since="8.19",note="Use Rinv_le_contravar.")]
Notation Rle_Rinv := Rle_Rinv_depr (only parsing).

#[deprecated(since="8.19",note="Use the bidirectional version Rlt_0_minus instead.")]
Notation Rlt_Rminus := (fun a b => proj2 (Rlt_0_minus a b)) (only parsing).

#[deprecated(since="8.19",note="Use the bidirectional version Rlt_0_minus instead.")]
Notation Rminus_gt_0_lt := (fun a b => proj1 (Rlt_0_minus a b)) (only parsing).

#[deprecated(since="8.19",note="Use Rdiv_opp_l.")]
Notation Ropp_div := (fun x y => Rdiv_opp_l x y) (only parsing).

Lemma Rplus_sqr_eq_0_l_depr : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0.
#[deprecated(since="8.19",note="Use Rplus_sqr_eq_0.")]
Notation Rplus_sqr_eq_0_l := Rplus_sqr_eq_0_l_depr (only parsing).

#[deprecated(since="8.19",note="Use Rplus_diag.")]
Notation double := (fun r1 => eq_sym (Rplus_diag r1)) (only parsing).

#[deprecated(since="8.19",note="Use Rplus_half_diag.")]
Notation double_var := (fun r1 => eq_sym (Rplus_half_diag r1)) (only parsing).

#[deprecated(since="8.19",note="Use eq_IZR_contrapositive.")]
Notation IZR_neq := (fun z1 z2 => (eq_IZR_contrapositive z1 z2)) (only parsing).

Lemma S_O_plus_INR_depr : forall n, INR (1 + n) = INR 1 + INR n.
#[deprecated(since="8.19")]
Notation S_O_plus_INR := S_O_plus_INR_depr (only parsing).

Lemma single_z_r_R1_depr :
  forall r (n m:Z),
    r < IZR n -> IZR n <= r + 1 -> r < IZR m -> IZR m <= r + 1 -> n = m.
#[deprecated(since="8.19")]
Notation single_z_r_R1 := single_z_r_R1_depr (only parsing).

Lemma tech_single_z_r_R1_depr :
  forall r (n:Z),
    r < IZR n ->
    IZR n <= r + 1 ->
    (exists s : Z, s <> n /\ r < IZR s /\ IZR s <= r + 1) -> False.
#[deprecated(since="8.19")]
Notation tech_single_z_r_R1 := tech_single_z_r_R1_depr (only parsing).

Lemma Rinv_mult_simpl_depr :
  forall r1 r2 r3, r1 <> 0 -> r1 * / r2 * (r3 * / r1) = r3 * / r2.
#[deprecated(since="8.19")]
Notation Rinv_mult_simpl := Rinv_mult_simpl_depr.