Library Coq.Reals.RIneq


Basic lemmas for the classical real numbers


Require Export Raxioms.
Require Import Rpow_def.
Require Import Zpower.
Require Export ZArithRing.
Require Import Omega.
Require Export RealField.

Local Open Scope Z_scope.
Local Open Scope R_scope.

Implicit Type r : R.

Relation between orders and equality

Reflexivity of the large order

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

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

Irreflexivity of the strict order

Lemma Rlt_irrefl : forall r, ~ r < r.
Hint Resolve Rlt_irrefl: real.

Lemma Rgt_irrefl : forall r, ~ r > r.

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: real.

Reasoning by case on equality and order
Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2.
Hint Resolve Req_dec: real.

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

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

Relating <, >, <= and >=

Order

Relating strict and large orders


Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
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.
Hint Immediate Rle_ge: real.
Hint Resolve Rle_ge: rorders.

Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1.
Hint Resolve Rge_le: real.
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_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1.
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.
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.
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 : forall r1 r2, r1 = r2 -> r1 <= r2.
Hint Immediate Req_le: real.

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

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

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

Asymmetry

Remark: Rlt_asym is an axiom

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

Antisymmetry


Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2.
Hint Resolve Rle_antisym: real.

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

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 an axiom

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.

(Classical) decidability


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 Rgt_ge_dec : forall r1 r2, {r1 > r2} + {r2 >= r1}.

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

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

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 Rle_lt_or_eq_dec : forall r1 r2, r1 <= r2 -> {r1 < r2} + {r1 = r2}.

Lemma inser_trans_R :
  forall r1 r2 r3 r4, r1 <= r2 < r3 -> {r1 <= r2 < r4} + {r4 <= r2 < r3}.

Addition

Remark: Rplus_0_l is an axiom

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

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


Remark: Rplus_opp_r is an axiom

Lemma Rplus_opp_l : forall r, - r + r = 0.
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)).

Hint Resolve f_equal_R : real.

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: 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_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.

Multiplication

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

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

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

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

Lemma Rmult_0_l : forall r, 0 * r = 0.
Hint Resolve Rmult_0_l: real.

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

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

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

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.
Hint Resolve Rmult_integral_contrapositive: real.

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.

Lemma Rsqr_0 : Rsqr 0 = 0.

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

Opposite

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

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

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

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

Lemma Ropp_neq_0_compat : forall r, r <> 0 -> - r <> 0.
Hint Resolve Ropp_neq_0_compat: real.

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

Opposite and multiplication


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

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

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

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: real.

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

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

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: real.

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

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

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

Lemma Rminus_eq_contra : forall r1 r2, r1 <> r2 -> r1 - r2 <> 0.
Hint Resolve Rminus_eq_contra: real.

Lemma Rminus_not_eq : forall r1 r2, r1 - r2 <> 0 -> r1 <> r2.
Hint Resolve Rminus_not_eq: real.

Lemma Rminus_not_eq_right : forall r1 r2, r2 - r1 <> 0 -> r1 <> r2.
Hint Resolve Rminus_not_eq_right: real.

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

Inverse


Lemma Rinv_1 : / 1 = 1.
Hint Resolve Rinv_1: real.

Lemma Rinv_neq_0_compat : forall r, r <> 0 -> / r <> 0.
Hint Resolve Rinv_neq_0_compat: real.

Lemma Rinv_involutive : forall r, r <> 0 -> / / r = r.
Hint Resolve Rinv_involutive: real.

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

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

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

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

Lemma Rinv_r_simpl_m : forall r1 r2, r1 <> 0 -> r1 * r2 * / r1 = r2.
Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: real.

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

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: real.

Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r.
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.
Hint Resolve Rplus_ge_compat_l: real.

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: 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.
Hint Immediate Rplus_lt_compat: real.

Lemma Rplus_le_compat :
  forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
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.

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 sum_inequa_Rle_lt :
  forall a x b c y d:R,
    a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.

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

Order and opposite

Contravariant compatibility


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

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

Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2.
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.
Hint Resolve Ropp_le_ge_contravar: real.

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

Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2.
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.
Hint Resolve Ropp_0_lt_gt_contravar: real.

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

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

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

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

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

Cancellation


Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
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.
Hint Immediate Ropp_le_cancel: real.

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.

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.
Hint Resolve Rmult_le_compat_l: real.

Lemma Rmult_le_compat_r :
  forall r r1 r2, 0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
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.
Hint Resolve Rmult_le_compat: real.

Lemma Rmult_ge_compat :
  forall r1 r2 r3 r4,
    r2 >= 0 -> r4 >= 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.

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_le_compat_neg_l :
  forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1.
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.
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.

Cancellation


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_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: real.

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

Lemma Rlt_Rminus : forall a b:R, 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:R), 0 <= r -> 0 < s -> r + s <> 0.
Hint Immediate tech_Rplus: real.

Order and square function


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

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

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

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.
Hint Resolve Rlt_0_1: real.

Lemma Rle_0_1 : 0 <= 1.

Order and inverse


Lemma Rinv_0_lt_compat : forall r, 0 < r -> 0 < / r.
Hint Resolve Rinv_0_lt_compat: real.

Lemma Rinv_lt_0_compat : forall r, r < 0 -> / r < 0.
Hint Resolve Rinv_lt_0_compat: real.

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

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

Miscellaneous

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

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

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 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.
Hint Resolve plus_INR: real.

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

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

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: real.

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

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

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

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

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

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

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

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

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

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

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

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

Injection from Z to R

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

Lemma INR_IPR : forall p, INR (Pos.to_nat p) = 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_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 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 : real.
Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : real.
Hint Extern 0 (IZR _ < IZR _) => apply IZR_lt, eq_refl : real.
Hint Extern 0 (IZR _ > IZR _) => apply IZR_lt, eq_refl : real.
Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, 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 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 ->
    (exists s : Z, s <> n /\ r < IZR s /\ IZR s <= r + 1) -> False.

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

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

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

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

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

Lemma double_var : forall r1, r1 = r1 / 2 + r1 / 2.

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 x y :
  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]).

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:R, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2.

Lemma completeness_weak :
  forall E:R -> Prop,
    bound E -> (exists x : R, E x) -> exists m : R, is_lub E m.

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

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 Req_EM_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.

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

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