Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(************************************************************************)

(*********************************************************)

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 
forall r : R, r <= r


forall r : R, r <= r

  intro; right; reflexivity.
Qed.
Hint Immediate Rle_refl: rorders.


forall r : R, r <= r


forall r : R, r <= r
 exact Rle_refl. Qed.
Hint Immediate Rge_refl: rorders.
Irreflexivity of the strict order 
forall r : R, ~ r < r


forall r : R, ~ r < r

  intros r H; eapply Rlt_asym; eauto.
Qed.
Hint Resolve Rlt_irrefl: real.


forall r : R, ~ r > r


forall r : R, ~ r > r
 exact Rlt_irrefl. Qed.


forall r1 r2 : R, r1 < r2 -> r1 <> r2


forall r1 r2 : R, r1 < r2 -> r1 <> r2

  
r1, r2:R
H:r1 < r2
H0:r1 = r2
r1 < r1

  pattern r1 at 2; rewrite H0; trivial.
Qed.


forall r1 r2 : R, r1 > r2 -> r1 <> r2


forall r1 r2 : R, r1 > r2 -> r1 <> r2

  intros; apply not_eq_sym; apply Rlt_not_eq; auto with real.
Qed.

(**********)

forall r1 r2 : R, r1 < r2 \/ r1 > r2 -> r1 <> r2


forall r1 r2 : R, r1 < r2 \/ r1 > r2 -> r1 <> r2

  
r1, r2:R
H0:r1 = r2
H1:r1 < r2
False
r1, r2:R
H0:r1 = r2
H1:r1 > r2
False

  
r1, r2:R
H0:r1 = r2
H1:r1 < r2
False
 
r1, r2:R
H0:r1 = r2
H1:r1 <> r2
False
 eauto.
  
r1, r2:R
H0:r1 = r2
H1:r1 > r2
False
 
r1, r2:R
H0:r1 = r2
H1:r1 <> r2
False
 eauto.
Qed.
Hint Resolve Rlt_dichotomy_converse: real.
Reasoning by case on equality and order 
(**********)

forall r1 r2 : R, r1 = r2 \/ r1 <> r2


forall r1 r2 : R, r1 = r2 \/ r1 <> r2

  intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse;
    unfold not; intuition eauto 3.
Qed.
Hint Resolve Req_dec: real.

(**********)

forall r1 r2 : R, r1 < r2 \/ r1 = r2 \/ r1 > r2


forall r1 r2 : R, r1 < r2 \/ r1 = r2 \/ r1 > r2

  intros; generalize (total_order_T r1 r2); tauto.
Qed.

(**********)

forall r1 r2 : R, r1 <> r2 -> r1 < r2 \/ r1 > r2


forall r1 r2 : R, r1 <> r2 -> r1 < r2 \/ r1 > r2

  intros; generalize (total_order_T r1 r2); tauto.
Qed.

(*********************************************************)

Relating <, >, ≤ and ≥

(*********************************************************)

(*********************************************************)

Order

(*********************************************************)

Relating strict and large orders

forall r1 r2 : R, r1 < r2 -> r1 <= r2


forall r1 r2 : R, r1 < r2 -> r1 <= r2

  intros; red; tauto.
Qed.
Hint Resolve Rlt_le: real.


forall r1 r2 : R, r1 > r2 -> r1 >= r2


forall r1 r2 : R, r1 > r2 -> r1 >= r2

  intros; red; tauto.
Qed.

(**********)

forall r1 r2 : R, r1 <= r2 -> r2 >= r1


forall r1 r2 : R, r1 <= r2 -> r2 >= r1

  destruct 1; red; auto with real.
Qed.
Hint Immediate Rle_ge: real.
Hint Resolve Rle_ge: rorders.


forall r1 r2 : R, r1 >= r2 -> r2 <= r1


forall r1 r2 : R, r1 >= r2 -> r2 <= r1

  destruct 1; red; auto with real.
Qed.
Hint Resolve Rge_le: real.
Hint Immediate Rge_le: rorders.

(**********)

forall r1 r2 : R, r1 < r2 -> r2 > r1


forall r1 r2 : R, r1 < r2 -> r2 > r1

  trivial.
Qed.
Hint Resolve Rlt_gt: rorders.


forall r1 r2 : R, r1 > r2 -> r2 < r1


forall r1 r2 : R, r1 > r2 -> r2 < r1

  trivial.
Qed.
Hint Immediate Rgt_lt: rorders.

(**********)


forall r1 r2 : R, ~ r1 <= r2 -> r2 < r1


forall r1 r2 : R, ~ r1 <= r2 -> r2 < r1

  intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle; tauto.
Qed.
Hint Immediate Rnot_le_lt: real.


forall r1 r2 : R, ~ r1 >= r2 -> r2 > r1


forall r1 r2 : R, ~ r1 >= r2 -> r2 > r1
 
r1, r2:R
H:~ r1 >= r2
~ r2 <= r1
 auto with real. Qed.


forall r1 r2 : R, ~ r1 <= r2 -> r1 > r2


forall r1 r2 : R, ~ r1 <= r2 -> r1 > r2
 
r1, r2:R
H:~ r1 <= r2
~ r1 <= r2
 auto with real. Qed.


forall r1 r2 : R, ~ r1 >= r2 -> r1 < r2


forall r1 r2 : R, ~ r1 >= r2 -> r1 < r2
 
r1, r2:R
H:~ r1 >= r2
~ r2 <= r1
 auto with real. Qed.


forall r1 r2 : R, ~ r1 < r2 -> r2 <= r1


forall r1 r2 : R, ~ r1 < r2 -> r2 <= r1

  
r1, r2:R
H:~ r1 < r2
H0:r1 < r2
r2 <= r1
r1, r2:R
H:~ r1 < r2
H0:r1 = r2
r2 <= r1
r1, r2:R
H:~ r1 < r2
H0:r1 > r2
r2 <= r1

    
r1, r2:R
H:~ r1 < r2
H0:r1 = r2
r2 <= r1
r1, r2:R
H:~ r1 < r2
H0:r1 > r2
r2 <= r1
 
r1, r2:R
H:~ r1 < r2
H0:r1 > r2
r2 <= r1
 auto with real.
Qed.


forall r1 r2 : R, ~ r1 > r2 -> r1 <= r2


forall r1 r2 : R, ~ r1 > r2 -> r1 <= r2
 auto using Rnot_lt_le with real. Qed.


forall r1 r2 : R, ~ r1 > r2 -> r2 >= r1


forall r1 r2 : R, ~ r1 > r2 -> r2 >= r1
 intros; eauto using Rnot_lt_le with rorders. Qed.


forall r1 r2 : R, ~ r1 < r2 -> r1 >= r2


forall r1 r2 : R, ~ r1 < r2 -> r1 >= r2
 eauto using Rnot_gt_ge with rorders. Qed.

(**********)

forall r1 r2 : R, r2 < r1 -> ~ r1 <= r2


forall r1 r2 : R, r2 < r1 -> ~ r1 <= r2

  
(forall r1 r2 : R, r1 < r2 -> ~ r2 < r1) ->
(forall r1 r2 : R, r1 < r2 \/ r1 > r2 -> r1 <> r2) ->
forall r1 r2 : R, r2 < r1 -> ~ (r1 < r2 \/ r1 = r2)

  unfold not; intuition eauto 3.
Qed.
Hint Immediate Rlt_not_le: real.


forall r1 r2 : R, r1 > r2 -> ~ r1 <= r2


forall r1 r2 : R, r1 > r2 -> ~ r1 <= r2
 exact Rlt_not_le. Qed.


forall r1 r2 : R, r1 < r2 -> ~ r1 >= r2


forall r1 r2 : R, r1 < r2 -> ~ r1 >= r2
 red; intros; eapply Rlt_not_le; eauto with real. Qed.
Hint Immediate Rlt_not_ge: real.


forall r1 r2 : R, r2 > r1 -> ~ r1 >= r2


forall r1 r2 : R, r2 > r1 -> ~ r1 >= r2
 exact Rlt_not_ge. Qed.


forall r1 r2 : R, r2 <= r1 -> ~ r1 < r2


forall r1 r2 : R, r2 <= r1 -> ~ r1 < r2

  
r1, r2:R
r2 <= r1 -> ~ r1 < r2
 
r1, r2:R
(r1 < r2 -> ~ r2 < r1) ->
(r1 < r2 \/ r1 > r2 -> r1 <> r2) ->
r2 <= r1 -> ~ r1 < r2

  unfold Rle; intuition.
Qed.


forall r1 r2 : R, r1 >= r2 -> ~ r1 < r2


forall r1 r2 : R, r1 >= r2 -> ~ r1 < r2
 intros; apply Rle_not_lt; auto with real. Qed.


forall r1 r2 : R, r1 <= r2 -> ~ r1 > r2


forall r1 r2 : R, r1 <= r2 -> ~ r1 > r2
 do 2 intro; apply Rle_not_lt. Qed.


forall r1 r2 : R, r2 >= r1 -> ~ r1 > r2


forall r1 r2 : R, r2 >= r1 -> ~ r1 > r2
 do 2 intro; apply Rge_not_lt. Qed.

(**********)

forall r1 r2 : R, r1 = r2 -> r1 <= r2


forall r1 r2 : R, r1 = r2 -> r1 <= r2

  unfold Rle; tauto.
Qed.
Hint Immediate Req_le: real.


forall r1 r2 : R, r1 = r2 -> r1 >= r2


forall r1 r2 : R, r1 = r2 -> r1 >= r2

  unfold Rge; tauto.
Qed.
Hint Immediate Req_ge: real.


forall r1 r2 : R, r2 = r1 -> r1 <= r2


forall r1 r2 : R, r2 = r1 -> r1 <= r2

  unfold Rle; auto.
Qed.
Hint Immediate Req_le_sym: real.


forall r1 r2 : R, r2 = r1 -> r1 >= r2


forall r1 r2 : R, r2 = r1 -> r1 >= r2

  unfold Rge; auto.
Qed.
Hint Immediate Req_ge_sym: real.

Asymmetry

Remark: Rlt_asym is an axiom 
forall r1 r2 : R, r1 > r2 -> ~ r2 > r1


forall r1 r2 : R, r1 > r2 -> ~ r2 > r1
 do 2 intro; apply Rlt_asym. Qed.

Antisymmetry

forall r1 r2 : R, r1 <= r2 -> r2 <= r1 -> r1 = r2


forall r1 r2 : R, r1 <= r2 -> r2 <= r1 -> r1 = r2

  intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle; intuition.
Qed.
Hint Resolve Rle_antisym: real.


forall r1 r2 : R, r1 >= r2 -> r2 >= r1 -> r1 = r2


forall r1 r2 : R, r1 >= r2 -> r2 >= r1 -> r1 = r2
 auto with real. Qed.

(**********)

forall r1 r2 : R, r1 <= r2 <= r1 <-> r1 = r2


forall r1 r2 : R, r1 <= r2 <= r1 <-> r1 = r2

  intuition.
Qed.


forall r1 r2 : R, r1 >= r2 /\ r2 >= r1 <-> r1 = r2


forall r1 r2 : R, r1 >= r2 /\ r2 >= r1 <-> r1 = r2

  intuition.
Qed.

Compatibility with equality

forall r1 r2 r3 r4 : R,
r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3


forall r1 r2 r3 r4 : R,
r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3

  intros x x' y y'; intros; replace x with x'; replace y with y'; assumption.
Qed.


forall r1 r2 r3 r4 : R,
r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3


forall r1 r2 r3 r4 : R,
r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3
 intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed.

Transitivity

Remark: Rlt_trans is an axiom 
forall r1 r2 r3 : R, r1 <= r2 -> r2 <= r3 -> r1 <= r3


forall r1 r2 r3 : R, r1 <= r2 -> r2 <= r3 -> r1 <= r3

  
(forall (A : Type) (x y z : A),
 x = y -> y = z -> x = z) ->
(forall r1 r2 r3 : R, r1 < r2 -> r2 < r3 -> r1 < r3) ->
(forall r1 r2 r3 r4 : R,
 r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3) ->
forall r1 r2 r3 : R, r1 <= r2 -> r2 <= r3 -> r1 <= r3

  
(forall (A : Type) (x y z : A),
 x = y -> y = z -> x = z) ->
(forall r1 r2 r3 : R, r1 < r2 -> r2 < r3 -> r1 < r3) ->
(forall r1 r2 r3 r4 : R,
 r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3) ->
forall r1 r2 r3 : R,
r1 < r2 \/ r1 = r2 ->
r2 < r3 \/ r2 = r3 -> r1 < r3 \/ r1 = r3

  intuition eauto 2.
Qed.


forall r1 r2 r3 : R, r1 >= r2 -> r2 >= r3 -> r1 >= r3


forall r1 r2 r3 : R, r1 >= r2 -> r2 >= r3 -> r1 >= r3
 eauto using Rle_trans with rorders. Qed.


forall r1 r2 r3 : R, r1 > r2 -> r2 > r3 -> r1 > r3


forall r1 r2 r3 : R, r1 > r2 -> r2 > r3 -> r1 > r3
 eauto using Rlt_trans with rorders. Qed.

(**********)

forall r1 r2 r3 : R, r1 <= r2 -> r2 < r3 -> r1 < r3


forall r1 r2 r3 : R, r1 <= r2 -> r2 < r3 -> r1 < r3

  
(forall r1 r2 r3 : R, r1 < r2 -> r2 < r3 -> r1 < r3) ->
(forall r1 r2 r3 r4 : R,
 r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3) ->
forall r1 r2 r3 : R, r1 <= r2 -> r2 < r3 -> r1 < r3

  
(forall r1 r2 r3 : R, r1 < r2 -> r2 < r3 -> r1 < r3) ->
(forall r1 r2 r3 r4 : R,
 r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3) ->
forall r1 r2 r3 : R,
r1 < r2 \/ r1 = r2 -> r2 < r3 -> r1 < r3

  intuition eauto 2.
Qed.


forall r1 r2 r3 : R, r1 < r2 -> r2 <= r3 -> r1 < r3


forall r1 r2 r3 : R, r1 < r2 -> r2 <= r3 -> r1 < r3

  generalize Rlt_trans Rlt_eq_compat; unfold Rle; intuition eauto 2.
Qed.


forall r1 r2 r3 : R, r1 >= r2 -> r2 > r3 -> r1 > r3


forall r1 r2 r3 : R, r1 >= r2 -> r2 > r3 -> r1 > r3
 eauto using Rlt_le_trans with rorders. Qed.


forall r1 r2 r3 : R, r1 > r2 -> r2 >= r3 -> r1 > r3


forall r1 r2 r3 : R, r1 > r2 -> r2 >= r3 -> r1 > r3
 eauto using Rle_lt_trans with rorders. Qed.

(Classical) decidability

forall r1 r2 : R, {r1 < r2} + {~ r1 < r2}


forall r1 r2 : R, {r1 < r2} + {~ r1 < r2}

  intros; generalize (total_order_T r1 r2) (Rlt_dichotomy_converse r1 r2);
    intuition.
Qed.


forall r1 r2 : R, {r1 <= r2} + {~ r1 <= r2}


forall r1 r2 : R, {r1 <= r2} + {~ r1 <= r2}

  
r1, r2:R
{r1 <= r2} + {~ r1 <= r2}

  
r1, r2:R
{r1 < r2} + {r1 = r2} + {r1 > r2} ->
(r1 < r2 \/ r1 > r2 -> r1 <> r2) ->
{r1 <= r2} + {~ r1 <= r2}

  intuition eauto 4 with real.
Qed.


forall r1 r2 : R, {r1 > r2} + {~ r1 > r2}


forall r1 r2 : R, {r1 > r2} + {~ r1 > r2}
 do 2 intro; apply Rlt_dec. Qed.


forall r1 r2 : R, {r1 >= r2} + {~ r1 >= r2}


forall r1 r2 : R, {r1 >= r2} + {~ r1 >= r2}
 intros; edestruct Rle_dec; [left|right]; eauto with rorders. Qed.


forall r1 r2 : R, {r1 < r2} + {r2 <= r1}


forall r1 r2 : R, {r1 < r2} + {r2 <= r1}

  intros; generalize (total_order_T r1 r2); intuition.
Qed.


forall r1 r2 : R, {r1 > r2} + {r2 >= r1}


forall r1 r2 : R, {r1 > r2} + {r2 >= r1}
 intros; edestruct Rlt_le_dec; [left|right]; eauto with rorders. Qed.


forall r1 r2 : R, {r1 <= r2} + {r2 < r1}


forall r1 r2 : R, {r1 <= r2} + {r2 < r1}

  intros; generalize (total_order_T r1 r2); intuition.
Qed.


forall r1 r2 : R, {r1 >= r2} + {r2 > r1}


forall r1 r2 : R, {r1 >= r2} + {r2 > r1}
 intros; edestruct Rle_lt_dec; [left|right]; eauto with rorders. Qed.


forall r1 r2 : R, r1 < r2 \/ r2 <= r1


forall r1 r2 : R, r1 < r2 \/ r2 <= r1

  intros n m; elim (Rle_lt_dec m n); auto with real.
Qed.


forall r1 r2 : R, r1 > r2 \/ r2 >= r1


forall r1 r2 : R, r1 > r2 \/ r2 >= r1
 intros; edestruct Rlt_or_le; [left|right]; eauto with rorders. Qed.


forall r1 r2 : R, r1 <= r2 \/ r2 < r1


forall r1 r2 : R, r1 <= r2 \/ r2 < r1

  intros n m; elim (Rlt_le_dec m n); auto with real.
Qed.


forall r1 r2 : R, r1 >= r2 \/ r2 > r1


forall r1 r2 : R, r1 >= r2 \/ r2 > r1
 intros; edestruct Rle_or_lt; [left|right]; eauto with rorders. Qed.


forall r1 r2 : R, r1 <= r2 -> {r1 < r2} + {r1 = r2}


forall r1 r2 : R, r1 <= r2 -> {r1 < r2} + {r1 = r2}

  intros r1 r2 H; generalize (total_order_T r1 r2); intuition.
Qed.

(**********)

forall r1 r2 r3 r4 : R,
r1 <= r2 < r3 -> {r1 <= r2 < r4} + {r4 <= r2 < r3}


forall r1 r2 r3 r4 : R,
r1 <= r2 < r3 -> {r1 <= r2 < r4} + {r4 <= r2 < r3}

  intros n m p q; intros; generalize (Rlt_le_dec m q); intuition.
Qed.

(*********************************************************)

Addition

(*********************************************************)
Remark: Rplus_0_l is an axiom 
forall r : R, r + 0 = r


forall r : R, r + 0 = r

  intro; ring.
Qed.
Hint Resolve Rplus_0_r: real.


forall r : R, r + 0 = r /\ 0 + r = r


forall r : R, r + 0 = r /\ 0 + r = r

  split; ring.
Qed.
Hint Resolve Rplus_ne: real.

(**********)
Remark: Rplus_opp_r is an axiom 
forall r : R, - r + r = 0


forall r : R, - r + r = 0

  intro; ring.
Qed.
Hint Resolve Rplus_opp_l: real.

(**********)

forall r1 r2 : R, r1 + r2 = 0 -> r2 = - r1


forall r1 r2 : R, r1 + r2 = 0 -> r2 = - r1

  
x, y:R
H:x + y = 0
- x + x + y = - x

  rewrite Rplus_assoc; rewrite H; ring.
Qed.

Definition f_equal_R := (f_equal (A:=R)).

Hint Resolve f_equal_R : real.


forall r r1 r2 : R, r1 = r2 -> r + r1 = r + r2


forall r r1 r2 : R, r1 = r2 -> r + r1 = r + r2

  
r, r1, r2:R
r1 = r2 -> r + r1 = r + r2

  apply f_equal.
Qed.


forall r r1 r2 : R, r1 = r2 -> r1 + r = r2 + r


forall r r1 r2 : R, r1 = r2 -> r1 + r = r2 + r

  
r, r1, r2:R
r1 = r2 -> r1 + r = r2 + r

  apply (f_equal (fun v => v + r)).
Qed.


(**********)

forall r r1 r2 : R, r + r1 = r + r2 -> r1 = r2


forall r r1 r2 : R, r + r1 = r + r2 -> r1 = r2

  
r, r1, r2:R
H:r + r1 = r + r2
r1 = - r + r + r1
r, r1, r2:R
H:r + r1 = r + r2
- r + r + r1 = r2

  
r, r1, r2:R
H:r + r1 = r + r2
- r + r + r1 = r2

  
r, r1, r2:R
H:r + r1 = r + r2
- r + r + r1 = - r + r + r2
r, r1, r2:R
H:r + r1 = r + r2
- r + r + r2 = r2

  
r, r1, r2:R
H:r + r1 = r + r2
- r + r + r2 = r2

  ring.
Qed.
Hint Resolve Rplus_eq_reg_l: real.


forall r r1 r2 : R, r1 + r = r2 + r -> r1 = r2


forall r r1 r2 : R, r1 + r = r2 + r -> r1 = r2

  
r, r1, r2:R
H:r1 + r = r2 + r
r1 = r2

  
r, r1, r2:R
H:r1 + r = r2 + r
r + r1 = r + r2

  now rewrite 2!(Rplus_comm r).
Qed.

(**********)

forall r r1 : R, r + r1 = r -> r1 = 0


forall r r1 : R, r + r1 = r -> r1 = 0

  intros r b; pattern r at 2; replace r with (r + 0); eauto with real.
Qed.

(***********)

forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0


forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0

  
a, b:R
H:0 <= a
H0:0 < b
H1:a + b = 0
a = 0
a, b:R
H:0 <= a
H0:0 = b
H1:a + b = 0
a = 0

    
a, b:R
H:0 <= a
H0:0 < b
H1:a + b = 0
~ 0 < a + b
a, b:R
H:0 <= a
H0:0 < b
H1:a + b = 0
0 < a + b
a, b:R
H:0 <= a
H0:0 = b
H1:a + b = 0
a = 0

      
a, b:R
H:0 <= a
H0:0 < b
H1:a + b = 0
0 < a + b
a, b:R
H:0 <= a
H0:0 = b
H1:a + b = 0
a = 0

      
a, b:R
H:0 <= a
H0:0 < b
H1:a + b = 0
0 <= a + 0
a, b:R
H:0 <= a
H0:0 < b
H1:a + b = 0
a + 0 < a + b
a, b:R
H:0 <= a
H0:0 = b
H1:a + b = 0
a = 0

        
a, b:R
H:0 <= a
H0:0 < b
H1:a + b = 0
a + 0 < a + b
a, b:R
H:0 <= a
H0:0 = b
H1:a + b = 0
a = 0

        
a, b:R
H:0 <= a
H0:0 = b
H1:a + b = 0
a = 0

    rewrite <- H0, Rplus_0_r in H1; assumption.
Qed.


forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0


forall r1 r2 : R,
0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0

  
a, b:R
H:0 <= a
H0:0 <= b
H1:a + b = 0
a = 0
a, b:R
H:0 <= a
H0:0 <= b
H1:a + b = 0
b = 0

  
a, b:R
H:0 <= a
H0:0 <= b
H1:a + b = 0
b = 0

  
a, b:R
H:0 <= a
H0:0 <= b
H1:a + b = 0
b + a = 0

  rewrite Rplus_comm; auto with real.
Qed.

(*********************************************************)

Multiplication

(*********************************************************)

(**********)

forall r : R, r <> 0 -> r * / r = 1


forall r : R, r <> 0 -> r * / r = 1

  intros; field; trivial.
Qed.
Hint Resolve Rinv_r: real.


forall r : R, r <> 0 -> 1 = / r * r


forall r : R, r <> 0 -> 1 = / r * r

  intros; field; trivial.
Qed.
Hint Resolve Rinv_l_sym: real.


forall r : R, r <> 0 -> 1 = r * / r


forall r : R, r <> 0 -> 1 = r * / r

  intros; field; trivial.
Qed.
Hint Resolve Rinv_r_sym: real.

(**********)

forall r : R, r * 0 = 0


forall r : R, r * 0 = 0

  intro; ring.
Qed.
Hint Resolve Rmult_0_r: real.

(**********)

forall r : R, 0 * r = 0


forall r : R, 0 * r = 0

  intro; ring.
Qed.
Hint Resolve Rmult_0_l: real.

(**********)

forall r : R, r * 1 = r /\ 1 * r = r


forall r : R, r * 1 = r /\ 1 * r = r

  intro; split; ring.
Qed.
Hint Resolve Rmult_ne: real.

(**********)

forall r : R, r * 1 = r


forall r : R, r * 1 = r

  intro; ring.
Qed.
Hint Resolve Rmult_1_r: real.

(**********)

forall r r1 r2 : R, r1 = r2 -> r * r1 = r * r2


forall r r1 r2 : R, r1 = r2 -> r * r1 = r * r2

  auto with real.
Qed.



forall r r1 r2 : R, r1 = r2 -> r1 * r = r2 * r


forall r r1 r2 : R, r1 = r2 -> r1 * r = r2 * r

  
r, r1, r2:R
H:r1 = r2
r1 * r = r2 * r

  
r, r1, r2:R
H:r1 = r2
r * r1 = r * r2

  now apply Rmult_eq_compat_l.
Qed.

(**********)

forall r r1 r2 : R,
r * r1 = r * r2 -> r <> 0 -> r1 = r2


forall r r1 r2 : R,
r * r1 = r * r2 -> r <> 0 -> r1 = r2

  
r, r1, r2:R
H:r * r1 = r * r2
H0:r <> 0
r1 = / r * r * r1
r, r1, r2:R
H:r * r1 = r * r2
H0:r <> 0
/ r * r * r1 = r2

  
r, r1, r2:R
H:r * r1 = r * r2
H0:r <> 0
/ r * r * r1 = r2

  
r, r1, r2:R
H:r * r1 = r * r2
H0:r <> 0
/ r * r * r1 = / r * r * r2
r, r1, r2:R
H:r * r1 = r * r2
H0:r <> 0
/ r * r * r2 = r2

  
r, r1, r2:R
H:r * r1 = r * r2
H0:r <> 0
/ r * r * r2 = r2

  field; trivial.
Qed.


forall r r1 r2 : R,
r1 * r = r2 * r -> r <> 0 -> r1 = r2


forall r r1 r2 : R,
r1 * r = r2 * r -> r <> 0 -> r1 = r2

  
r, r1, r2:R
H:r1 * r = r2 * r
H0:r <> 0
r1 = r2

  
r, r1, r2:R
H:r1 * r = r2 * r
H0:r <> 0
r * r1 = r * r2

  now rewrite 2!(Rmult_comm r).
Qed.

(**********)

forall r1 r2 : R, r1 * r2 = 0 -> r1 = 0 \/ r2 = 0


forall r1 r2 : R, r1 * r2 = 0 -> r1 = 0 \/ r2 = 0

  
r1, r2:R
H:r1 * r2 = 0
Hz:r1 = 0
r1 = 0 \/ r2 = 0
r1, r2:R
H:r1 * r2 = 0
Hnotz:r1 <> 0
r1 = 0 \/ r2 = 0

  
r1, r2:R
H:r1 * r2 = 0
Hnotz:r1 <> 0
r1 = 0 \/ r2 = 0

  
r1, r2:R
H:r1 * r2 = 0
Hnotz:r1 <> 0
r1 * r2 = r1 * 0

  rewrite H; auto with real.
Qed.

(**********)

forall r1 r2 : R, r1 = 0 \/ r2 = 0 -> r1 * r2 = 0


forall r1 r2 : R, r1 = 0 \/ r2 = 0 -> r1 * r2 = 0

  intros r1 r2 [H| H]; rewrite H; auto with real.
Qed.

Hint Resolve Rmult_eq_0_compat: real.

(**********)

forall r1 r2 : R, r1 = 0 -> r1 * r2 = 0


forall r1 r2 : R, r1 = 0 -> r1 * r2 = 0

  auto with real.
Qed.

(**********)

forall r1 r2 : R, r2 = 0 -> r1 * r2 = 0


forall r1 r2 : R, r2 = 0 -> r1 * r2 = 0

  auto with real.
Qed.

(**********)

forall r1 r2 : R, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0


forall r1 r2 : R, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0

  intros r1 r2 H; split; red; intro; apply H; auto with real.
Qed.

(**********)

forall r1 r2 : R, r1 <> 0 /\ r2 <> 0 -> r1 * r2 <> 0


forall r1 r2 : R, r1 <> 0 /\ r2 <> 0 -> r1 * r2 <> 0

  
r1, r2:R
H1:r1 <> 0
H2:r2 <> 0
H:r1 * r2 = 0
False

  case (Rmult_integral r1 r2); auto with real.
Qed.
Hint Resolve Rmult_integral_contrapositive: real.


forall r1 r2 : R, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0


forall r1 r2 : R, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0
 auto using Rmult_integral_contrapositive. Qed.

(**********)

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


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

  intros; ring.
Qed.

(*********************************************************)

Square function

(*********************************************************)

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

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

(***********)

0² = 0

  unfold Rsqr; auto with real.
Qed.

(***********)

forall r : R, r² = 0 -> r = 0

  unfold Rsqr; intros; elim (Rmult_integral r r H); trivial.
Qed.

(*********************************************************)

Opposite

(*********************************************************)

(**********)

forall r1 r2 : R, r1 = r2 -> - r1 = - r2


forall r1 r2 : R, r1 = r2 -> - r1 = - r2

  auto with real.
Qed.
Hint Resolve Ropp_eq_compat: real.

(**********)

- 0 = 0


- 0 = 0

  ring.
Qed.
Hint Resolve Ropp_0: real.

(**********)

forall r : R, r = 0 -> - r = 0


forall r : R, r = 0 -> - r = 0

  intros; rewrite H; auto with real.
Qed.
Hint Resolve Ropp_eq_0_compat: real.

(**********)

forall r : R, - - r = r


forall r : R, - - r = r

  intro; ring.
Qed.
Hint Resolve Ropp_involutive: real.

(*********)

forall r : R, r <> 0 -> - r <> 0


forall r : R, r <> 0 -> - r <> 0

  
r:R
H:r <> 0
H0:- r = 0
False

  
r:R
H:r <> 0
H0:- r = 0
r = 0

  transitivity (- - r); auto with real.
Qed.
Hint Resolve Ropp_neq_0_compat: real.

(**********)

forall r1 r2 : R, - (r1 + r2) = - r1 + - r2


forall r1 r2 : R, - (r1 + r2) = - r1 + - r2

  intros; ring.
Qed.
Hint Resolve Ropp_plus_distr: real.

(*********************************************************)

Opposite and multiplication

(*********************************************************)


forall r1 r2 : R, - (r1 * r2) = - r1 * r2


forall r1 r2 : R, - (r1 * r2) = - r1 * r2

  intros; ring.
Qed.


forall r1 r2 : R, - r1 * r2 = - (r1 * r2)


forall r1 r2 : R, - r1 * r2 = - (r1 * r2)

  intros; ring.
Qed.
Hint Resolve Ropp_mult_distr_l_reverse: real.

(**********)

forall r1 r2 : R, - r1 * - r2 = r1 * r2


forall r1 r2 : R, - r1 * - r2 = r1 * r2

  intros; ring.
Qed.
Hint Resolve Rmult_opp_opp: real.


forall r1 r2 : R, - (r1 * r2) = r1 * - r2


forall r1 r2 : R, - (r1 * r2) = r1 * - r2

  intros; ring.
Qed.


forall r1 r2 : R, r1 * - r2 = - (r1 * r2)


forall r1 r2 : R, r1 * - r2 = - (r1 * r2)

  intros; ring.
Qed.

(*********************************************************)

Subtraction

(*********************************************************)


forall r : R, r - 0 = r


forall r : R, r - 0 = r

  intro; ring.
Qed.
Hint Resolve Rminus_0_r: real.


forall r : R, 0 - r = - r


forall r : R, 0 - r = - r

  intro; ring.
Qed.
Hint Resolve Rminus_0_l: real.

(**********)

forall r1 r2 : R, - (r1 - r2) = r2 - r1


forall r1 r2 : R, - (r1 - r2) = r2 - r1

  intros; ring.
Qed.
Hint Resolve Ropp_minus_distr: real.


forall r1 r2 : R, - (r2 - r1) = r1 - r2


forall r1 r2 : R, - (r2 - r1) = r1 - r2

  intros; ring.
Qed.

(**********)

forall r1 r2 : R, r1 = r2 -> r1 - r2 = 0


forall r1 r2 : R, r1 = r2 -> r1 - r2 = 0

  intros; rewrite H; ring.
Qed.
Hint Resolve Rminus_diag_eq: real.

(**********)

forall r1 r2 : R, r1 - r2 = 0 -> r1 = r2


forall r1 r2 : R, r1 - r2 = 0 -> r1 = r2

  
r1, r2:R
H:- r2 + r1 = 0
r1 = r2

  rewrite <- (Ropp_involutive r2); apply (Rplus_opp_r_uniq (- r2) r1 H).
Qed.
Hint Immediate Rminus_diag_uniq: real.


forall r1 r2 : R, r2 - r1 = 0 -> r1 = r2


forall r1 r2 : R, r2 - r1 = 0 -> r1 = r2

  intros; generalize (Rminus_diag_uniq r2 r1 H); clear H; intro H; rewrite H;
    ring.
Qed.
Hint Immediate Rminus_diag_uniq_sym: real.


forall r1 r2 : R, r1 + (r2 - r1) = r2


forall r1 r2 : R, r1 + (r2 - r1) = r2

  intros; ring.
Qed.
Hint Resolve Rplus_minus: real.

(**********)

forall r1 r2 : R, r1 <> r2 -> r1 - r2 <> 0


forall r1 r2 : R, r1 <> r2 -> r1 - r2 <> 0

  
r1, r2:R
H:r1 <> r2
H0:r1 - r2 = 0
False

  apply H; auto with real.
Qed.
Hint Resolve Rminus_eq_contra: real.


forall r1 r2 : R, r1 - r2 <> 0 -> r1 <> r2


forall r1 r2 : R, r1 - r2 <> 0 -> r1 <> r2

  red; intros; elim H; apply Rminus_diag_eq; auto.
Qed.
Hint Resolve Rminus_not_eq: real.


forall r1 r2 : R, r2 - r1 <> 0 -> r1 <> r2


forall r1 r2 : R, r2 - r1 <> 0 -> r1 <> r2

  red; intros; elim H; rewrite H0; ring.
Qed.
Hint Resolve Rminus_not_eq_right: real.

(**********)

forall r1 r2 r3 : R,
r1 * (r2 - r3) = r1 * r2 - r1 * r3


forall r1 r2 r3 : R,
r1 * (r2 - r3) = r1 * r2 - r1 * r3

  intros; ring.
Qed.

(*********************************************************)

Inverse

(*********************************************************)


/ 1 = 1


/ 1 = 1

  field.
Qed.
Hint Resolve Rinv_1: real.

(*********)

forall r : R, r <> 0 -> / r <> 0


forall r : R, r <> 0 -> / r <> 0

  
r:R
H:r <> 0
H0:/ r = 0
1 = 0

  replace 1 with (/ r * r); auto with real.
Qed.
Hint Resolve Rinv_neq_0_compat: real.

(*********)

forall r : R, r <> 0 -> / / r = r


forall r : R, r <> 0 -> / / r = r

  intros; field; trivial.
Qed.
Hint Resolve Rinv_involutive: real.

(*********)

forall r1 r2 : R,
r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2


forall r1 r2 : R,
r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2

  intros; field; auto.  
Qed.

(*********)

forall r : R, r <> 0 -> - / r = / - r


forall r : R, r <> 0 -> - / r = / - r

  intros; field; trivial.
Qed.


forall r1 r2 : R, r1 <> 0 -> r1 * / r1 * r2 = r2


forall r1 r2 : R, r1 <> 0 -> r1 * / r1 * r2 = r2

  
r1, r2:R
H:r1 <> 0
r1 * / r1 * r2 = 1 * r2

  rewrite Rinv_r; auto with real.
Qed.


forall r1 r2 : R, r1 <> 0 -> r2 * r1 * / r1 = r2


forall r1 r2 : R, r1 <> 0 -> r2 * r1 * / r1 = r2

  
r1, r2:R
H:r1 <> 0
r2 * r1 * / r1 = r2 * 1

  transitivity (r2 * (r1 * / r1)); auto with real.
Qed.


forall r1 r2 : R, r1 <> 0 -> r1 * r2 * / r1 = r2


forall r1 r2 : R, r1 <> 0 -> r1 * r2 * / r1 = r2

  
r1, r2:R
H:r1 <> 0
r1 * r2 * / r1 = r2 * 1

  
r1, r2:R
H:r1 <> 0
r1 * r2 * / r1 = r2 * (r1 * / r1)

  ring.
Qed.
Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: real.

(*********)

forall r1 r2 r3 : R,
r1 <> 0 -> r1 * / r2 * (r3 * / r1) = r3 * / r2


forall r1 r2 r3 : R,
r1 <> 0 -> r1 * / r2 * (r3 * / r1) = r3 * / r2

  
a, b, c:R
H:a <> 0
a * / b * (c * / a) = c * / b

  
a, b, c:R
H:a <> 0
a * / b * (c * / a) = a * / a * (c * / b)

  ring.
Qed.

(*********************************************************)

Order and addition

(*********************************************************)

Compatibility

Remark: Rplus_lt_compat_l is an axiom 
forall r r1 r2 : R, r1 > r2 -> r + r1 > r + r2


forall r r1 r2 : R, r1 > r2 -> r + r1 > r + r2
 eauto using Rplus_lt_compat_l with rorders. Qed.
Hint Resolve Rplus_gt_compat_l: real.

(**********)

forall r r1 r2 : R, r1 < r2 -> r1 + r < r2 + r


forall r r1 r2 : R, r1 < r2 -> r1 + r < r2 + r

  
r, r1, r2:R
H:r1 < r2
r1 + r < r2 + r

  rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r); auto with real.
Qed.
Hint Resolve Rplus_lt_compat_r: real.


forall r r1 r2 : R, r1 > r2 -> r1 + r > r2 + r


forall r r1 r2 : R, r1 > r2 -> r1 + r > r2 + r
 do 3 intro; apply Rplus_lt_compat_r. Qed.

(**********)

forall r r1 r2 : R, r1 <= r2 -> r + r1 <= r + r2


forall r r1 r2 : R, r1 <= r2 -> r + r1 <= r + r2

  
r, r1, r2:R
H:r1 < r2 \/ r1 = r2
H0:r1 < r2
r + r1 < r + r2 \/ r + r1 = r + r2
r, r1, r2:R
H:r1 < r2 \/ r1 = r2
H0:r1 = r2
r + r1 < r + r2 \/ r + r1 = r + r2

  
r, r1, r2:R
H:r1 < r2 \/ r1 = r2
H0:r1 = r2
r + r1 < r + r2 \/ r + r1 = r + r2

  right; rewrite <- H0; auto with zarith real.
Qed.


forall r r1 r2 : R, r1 >= r2 -> r + r1 >= r + r2


forall r r1 r2 : R, r1 >= r2 -> r + r1 >= r + r2
 auto using Rplus_le_compat_l with rorders. Qed.
Hint Resolve Rplus_ge_compat_l: real.

(**********)

forall r r1 r2 : R, r1 <= r2 -> r1 + r <= r2 + r


forall r r1 r2 : R, r1 <= r2 -> r1 + r <= r2 + r

  
r, r1, r2:R
H:r1 < r2 \/ r1 = r2
H0:r1 < r2
r1 + r < r2 + r \/ r1 + r = r2 + r
r, r1, r2:R
H:r1 < r2 \/ r1 = r2
H0:r1 = r2
r1 + r < r2 + r \/ r1 + r = r2 + r

  
r, r1, r2:R
H:r1 < r2 \/ r1 = r2
H0:r1 = r2
r1 + r < r2 + r \/ r1 + r = r2 + r

  right; rewrite <- H0; auto with real.
Qed.

Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real.


forall r r1 r2 : R, r1 >= r2 -> r1 + r >= r2 + r


forall r r1 r2 : R, r1 >= r2 -> r1 + r >= r2 + r
 auto using Rplus_le_compat_r with rorders. Qed.

(*********)

forall r1 r2 r3 r4 : R,
r1 < r2 -> r3 < r4 -> r1 + r3 < r2 + r4


forall r1 r2 r3 r4 : R,
r1 < r2 -> r3 < r4 -> r1 + r3 < r2 + r4

  intros; apply Rlt_trans with (r2 + r3); auto with real.
Qed.
Hint Immediate Rplus_lt_compat: real.


forall r1 r2 r3 r4 : R,
r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4


forall r1 r2 r3 r4 : R,
r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4

  intros; apply Rle_trans with (r2 + r3); auto with real.
Qed.
Hint Immediate Rplus_le_compat: real.


forall r1 r2 r3 r4 : R,
r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4


forall r1 r2 r3 r4 : R,
r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4
 auto using Rplus_lt_compat with rorders. Qed.


forall r1 r2 r3 r4 : R,
r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4


forall r1 r2 r3 r4 : R,
r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4
 auto using Rplus_le_compat with rorders. Qed.

(*********)

forall r1 r2 r3 r4 : R,
r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4


forall r1 r2 r3 r4 : R,
r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4

  intros; apply Rlt_le_trans with (r2 + r3); auto with real.
Qed.


forall r1 r2 r3 r4 : R,
r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4


forall r1 r2 r3 r4 : R,
r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4

  intros; apply Rle_lt_trans with (r2 + r3); auto with real.
Qed.

Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: real.


forall r1 r2 r3 r4 : R,
r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4


forall r1 r2 r3 r4 : R,
r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4
 auto using Rplus_lt_le_compat with rorders. Qed.


forall r1 r2 r3 r4 : R,
r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4


forall r1 r2 r3 r4 : R,
r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4
 auto using Rplus_le_lt_compat with rorders. Qed.

(**********)

forall r1 r2 : R, 0 < r1 -> 0 < r2 -> 0 < r1 + r2


forall r1 r2 : R, 0 < r1 -> 0 < r2 -> 0 < r1 + r2

  intros x y; intros; apply Rlt_trans with x;
    [ assumption
      | pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
        assumption ].
Qed.


forall r1 r2 : R, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2


forall r1 r2 : R, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2

  intros x y; intros; apply Rle_lt_trans with x;
    [ assumption
      | pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
        assumption ].
Qed.


forall r1 r2 : R, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2


forall r1 r2 : R, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2

  intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat;
    assumption.
Qed.


forall r1 r2 : R, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2


forall r1 r2 : R, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2

  intros x y; intros; apply Rle_trans with x;
    [ assumption
      | pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
        assumption ].
Qed.

(**********)

forall a x b c y d : R,
a <= x ->
x < b -> c < y -> y <= d -> a + c < x + y < b + d


forall a x b c y d : R,
a <= x ->
x < b -> c < y -> y <= d -> a + c < x + y < b + d

  
a, x, b, c, y, d:R
H:a <= x
H0:x < b
H1:c < y
H2:y <= d
a + c < x + y
a, x, b, c, y, d:R
H:a <= x
H0:x < b
H1:c < y
H2:y <= d
x + y < b + d

  
a, x, b, c, y, d:R
H:a <= x
H0:x < b
H1:c < y
H2:y <= d
x + y < b + d

  apply Rlt_le_trans with (b + y); auto with real.
Qed.

Cancellation

forall r r1 r2 : R, r + r1 < r + r2 -> r1 < r2


forall r r1 r2 : R, r + r1 < r + r2 -> r1 < r2

  
r, r1, r2:R
H:r + r1 < r + r2
- r + r + r1 < - r + r + r2 -> r1 < r2
r, r1, r2:R
H:r + r1 < r + r2
- r + r + r1 < - r + r + r2

  
r, r1, r2:R
H:r + r1 < r + r2
0 + r1 < 0 + r2 -> r1 < r2
r, r1, r2:R
H:r + r1 < r + r2
- r + r + r1 < - r + r + r2

  
r, r1, r2:R
H:r + r1 < r + r2
- r + r + r1 < - r + r + r2

  rewrite Rplus_assoc; rewrite Rplus_assoc;
    apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H).
Qed.


forall r r1 r2 : R, r1 + r < r2 + r -> r1 < r2


forall r r1 r2 : R, r1 + r < r2 + r -> r1 < r2

  
r, r1, r2:R
H:r1 + r < r2 + r
r1 < r2

  
r, r1, r2:R
H:r1 + r < r2 + r
r + r1 < r + r2

  now rewrite 2!(Rplus_comm r).
Qed.


forall r r1 r2 : R, r + r1 <= r + r2 -> r1 <= r2


forall r r1 r2 : R, r + r1 <= r + r2 -> r1 <= r2

  
r, r1, r2:R
H:r + r1 < r + r2 \/ r + r1 = r + r2
H0:r + r1 < r + r2
r1 < r2 \/ r1 = r2
r, r1, r2:R
H:r + r1 < r + r2 \/ r + r1 = r + r2
H0:r + r1 = r + r2
r1 < r2 \/ r1 = r2

  
r, r1, r2:R
H:r + r1 < r + r2 \/ r + r1 = r + r2
H0:r + r1 = r + r2
r1 < r2 \/ r1 = r2

  right; apply (Rplus_eq_reg_l r r1 r2 H0).
Qed.


forall r r1 r2 : R, r1 + r <= r2 + r -> r1 <= r2


forall r r1 r2 : R, r1 + r <= r2 + r -> r1 <= r2

  
r, r1, r2:R
H:r1 + r <= r2 + r
r1 <= r2

  
r, r1, r2:R
H:r1 + r <= r2 + r
r + r1 <= r + r2

  now rewrite 2!(Rplus_comm r).
Qed.


forall r r1 r2 : R, r + r1 > r + r2 -> r1 > r2


forall r r1 r2 : R, r + r1 > r + r2 -> r1 > r2

  unfold Rgt; intros; apply (Rplus_lt_reg_l r r2 r1 H).
Qed.


forall r r1 r2 : R, r + r1 >= r + r2 -> r1 >= r2


forall r r1 r2 : R, r + r1 >= r + r2 -> r1 >= r2

  intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real.
Qed.

(**********)

forall r1 r2 r3 : R,
0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3


forall r1 r2 r3 : R,
0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3

  intros x y z; intros; apply Rle_trans with (x + y);
    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
      assumption
      | assumption ].
Qed.


forall r1 r2 r3 : R,
0 <= r2 -> r1 + r2 < r3 -> r1 < r3


forall r1 r2 r3 : R,
0 <= r2 -> r1 + r2 < r3 -> r1 < r3

  intros x y z; intros; apply Rle_lt_trans with (x + y);
    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
      assumption
      | assumption ].
Qed.


forall r1 r2 r3 : R,
0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3


forall r1 r2 r3 : R,
0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3

  intros x y z; intros; apply Rge_trans with (x + y);
    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l;
      assumption
      | assumption ].
Qed.


forall r1 r2 r3 : R,
0 >= r2 -> r1 + r2 > r3 -> r1 > r3


forall r1 r2 r3 : R,
0 >= r2 -> r1 + r2 > r3 -> r1 > r3

  intros x y z; intros; apply Rge_gt_trans with (x + y);
    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l;
      assumption
      | assumption ].
Qed.

(*********************************************************)

Order and opposite

(*********************************************************)

Contravariant compatibility

forall r1 r2 : R, r1 > r2 -> - r1 < - r2


forall r1 r2 : R, r1 > r2 -> - r1 < - r2

  
r1, r2:R
H:r2 < r1
- r1 < - r2

  
r1, r2:R
H:r2 < r1
r2 + r1 + - r1 < r2 + r1 + - r2

  
r1, r2:R
H:r2 < r1
r2 < r2 + r1 + - r2

  
r1, r2:R
H:r2 < r1
r2 < r1

  exact H.
Qed.
Hint Resolve Ropp_gt_lt_contravar : core.


forall r1 r2 : R, r1 < r2 -> - r1 > - r2


forall r1 r2 : R, r1 < r2 -> - r1 > - r2

  unfold Rgt; auto with real.
Qed.
Hint Resolve Ropp_lt_gt_contravar: real.

(**********)

forall r1 r2 : R, r2 < r1 -> - r1 < - r2


forall r1 r2 : R, r2 < r1 -> - r1 < - r2

  auto with real.
Qed.
Hint Resolve Ropp_lt_contravar: real.


forall r1 r2 : R, r2 > r1 -> - r1 > - r2


forall r1 r2 : R, r2 > r1 -> - r1 > - r2
 auto with real. Qed.

(**********)

forall r1 r2 : R, r1 <= r2 -> - r1 >= - r2


forall r1 r2 : R, r1 <= r2 -> - r1 >= - r2

  unfold Rge; intros r1 r2 [H| H]; auto with real.
Qed.
Hint Resolve Ropp_le_ge_contravar: real.


forall r1 r2 : R, r1 >= r2 -> - r1 <= - r2


forall r1 r2 : R, r1 >= r2 -> - r1 <= - r2

  unfold Rle; intros r1 r2 [H| H]; auto with real.
Qed.
Hint Resolve Ropp_ge_le_contravar: real.

(**********)

forall r1 r2 : R, r2 <= r1 -> - r1 <= - r2


forall r1 r2 : R, r2 <= r1 -> - r1 <= - r2

  intros r1 r2 H; elim H; auto with real.
Qed.
Hint Resolve Ropp_le_contravar: real.


forall r1 r2 : R, r2 >= r1 -> - r1 >= - r2


forall r1 r2 : R, r2 >= r1 -> - r1 >= - r2
 auto using Ropp_le_contravar with real. Qed.

(**********)

forall r : R, 0 < r -> 0 > - r


forall r : R, 0 < r -> 0 > - r

  intros; replace 0 with (-0); auto with real.
Qed.
Hint Resolve Ropp_0_lt_gt_contravar: real.


forall r : R, 0 > r -> 0 < - r


forall r : R, 0 > r -> 0 < - r

  intros; replace 0 with (-0); auto with real.
Qed.
Hint Resolve Ropp_0_gt_lt_contravar: real.

(**********)

forall r : R, r > 0 -> - r < 0


forall r : R, r > 0 -> - r < 0

  intros; rewrite <- Ropp_0; auto with real.
Qed.
Hint Resolve Ropp_lt_gt_0_contravar: real.


forall r : R, r < 0 -> - r > 0


forall r : R, r < 0 -> - r > 0

  intros; rewrite <- Ropp_0; auto with real.
Qed.
Hint Resolve Ropp_gt_lt_0_contravar: real.

(**********)

forall r : R, 0 <= r -> 0 >= - r


forall r : R, 0 <= r -> 0 >= - r

  intros; replace 0 with (-0); auto with real.
Qed.
Hint Resolve Ropp_0_le_ge_contravar: real.


forall r : R, 0 >= r -> 0 <= - r


forall r : R, 0 >= r -> 0 <= - r

  intros; replace 0 with (-0); auto with real.
Qed.
Hint Resolve Ropp_0_ge_le_contravar: real.

Cancellation

forall r1 r2 : R, - r2 < - r1 -> r1 < r2


forall r1 r2 : R, - r2 < - r1 -> r1 < r2

  
x, y:R
H':- y < - x
x < y

  rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
    auto with real.
Qed.
Hint Immediate Ropp_lt_cancel: real.


forall r1 r2 : R, - r2 > - r1 -> r1 > r2


forall r1 r2 : R, - r2 > - r1 -> r1 > r2
 auto using Ropp_lt_cancel with rorders. Qed.


forall r1 r2 : R, - r2 <= - r1 -> r1 <= r2


forall r1 r2 : R, - r2 <= - r1 -> r1 <= r2

  
x, y:R
H:- y <= - x
x <= y

  
x, y:R
H:- y <= - x
- y = - x -> x <= y

  intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
    rewrite H1; auto with real.
Qed.
Hint Immediate Ropp_le_cancel: real.


forall r1 r2 : R, - r2 >= - r1 -> r1 >= r2


forall r1 r2 : R, - r2 >= - r1 -> r1 >= r2
 auto using Ropp_le_cancel with rorders. Qed.

(*********************************************************)

Order and multiplication

(*********************************************************)
Remark: Rmult_lt_compat_l is an axiom

Covariant compatibility

forall r r1 r2 : R,
0 < r -> r1 < r2 -> r1 * r < r2 * r


forall r r1 r2 : R,
0 < r -> r1 < r2 -> r1 * r < r2 * r

  intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real.
Qed.
Hint Resolve Rmult_lt_compat_r : core.


forall r r1 r2 : R,
r > 0 -> r1 > r2 -> r1 * r > r2 * r


forall r r1 r2 : R,
r > 0 -> r1 > r2 -> r1 * r > r2 * r
 eauto using Rmult_lt_compat_r with rorders. Qed.


forall r r1 r2 : R,
r > 0 -> r1 > r2 -> r * r1 > r * r2


forall r r1 r2 : R,
r > 0 -> r1 > r2 -> r * r1 > r * r2
 eauto using Rmult_lt_compat_l with rorders. Qed.

(**********)

forall r r1 r2 : R,
0 <= r -> r1 <= r2 -> r * r1 <= r * r2


forall r r1 r2 : R,
0 <= r -> r1 <= r2 -> r * r1 <= r * r2

  
r, r1, r2:R
H:0 = r
H0:r1 < r2
r * r1 < r * r2 \/ r * r1 = r * r2

  right; rewrite <- H; do 2 rewrite Rmult_0_l; reflexivity.
Qed.
Hint Resolve Rmult_le_compat_l: real.


forall r r1 r2 : R,
0 <= r -> r1 <= r2 -> r1 * r <= r2 * r


forall r r1 r2 : R,
0 <= r -> r1 <= r2 -> r1 * r <= r2 * r

  intros r r1 r2 H; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r);
    auto with real.
Qed.
Hint Resolve Rmult_le_compat_r: real.


forall r r1 r2 : R,
r >= 0 -> r1 >= r2 -> r * r1 >= r * r2


forall r r1 r2 : R,
r >= 0 -> r1 >= r2 -> r * r1 >= r * r2
 eauto using Rmult_le_compat_l with rorders. Qed.


forall r r1 r2 : R,
r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r


forall r r1 r2 : R,
r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r
 eauto using Rmult_le_compat_r with rorders. Qed.

(**********)

forall r1 r2 r3 r4 : R,
0 <= r1 ->
0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4


forall r1 r2 r3 r4 : R,
0 <= r1 ->
0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4

  
x, y, z, t:R
H':0 <= x
H'0:0 <= z
H'1:x <= y
H'2:z <= t
x * z <= y * t

  
x, y, z, t:R
H':0 <= x
H'0:0 <= z
H'1:x <= y
H'2:z <= t
x * t <= y * t

  
x, y, z, t:R
H':0 <= x
H'0:0 <= z
H'1:x <= y
H'2:z <= t
t * x <= t * y

  
x, y, z, t:R
H':0 <= x
H'0:0 <= z
H'1:x <= y
H'2:z <= t
0 <= t

  apply Rle_trans with z; auto.
Qed.
Hint Resolve Rmult_le_compat: real.


forall r1 r2 r3 r4 : R,
r2 >= 0 ->
r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4


forall r1 r2 r3 r4 : R,
r2 >= 0 ->
r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4
 auto with real rorders. Qed.


forall r1 r2 r3 r4 : R,
r3 > 0 ->
r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4


forall r1 r2 r3 r4 : R,
r3 > 0 ->
r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4

  intros; apply Rlt_trans with (r2 * r3); auto with real.
Qed.

(*********)

forall r1 r2 r3 r4 : R,
0 <= r1 ->
0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4


forall r1 r2 r3 r4 : R,
0 <= r1 ->
0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4

  intros; apply Rle_lt_trans with (r2 * r3);
    [ apply Rmult_le_compat_r; [ assumption | left; assumption ]
      | apply Rmult_lt_compat_l;
        [ apply Rle_lt_trans with r1; assumption | assumption ] ].
Qed.

(*********)

forall r1 r2 : R, 0 < r1 -> 0 < r2 -> 0 < r1 * r2


forall r1 r2 : R, 0 < r1 -> 0 < r2 -> 0 < r1 * r2
 intros; replace 0 with (0 * r2); auto with real. Qed.


forall r1 r2 : R, r1 > 0 -> r2 > 0 -> r1 * r2 > 0

Proof Rmult_lt_0_compat.

Contravariant compatibility

forall r r1 r2 : R,
r <= 0 -> r1 <= r2 -> r * r2 <= r * r1


forall r r1 r2 : R,
r <= 0 -> r1 <= r2 -> r * r2 <= r * r1

  
r, r1, r2:R
H:r <= 0
H0:r1 <= r2
- - r * r2 <= - - r * r1

  
r, r1, r2:R
H:r <= 0
H0:r1 <= r2
- (- r * r2) <= - (- r * r1)

  apply Ropp_le_contravar; auto with real.
Qed.
Hint Resolve Rmult_le_compat_neg_l: real.


forall r r1 r2 : R,
r <= 0 -> r1 <= r2 -> r * r1 >= r * r2


forall r r1 r2 : R,
r <= 0 -> r1 <= r2 -> r * r1 >= r * r2

  intros; apply Rle_ge; auto with real.
Qed.
Hint Resolve Rmult_le_ge_compat_neg_l: real.


forall r r1 r2 : R,
r < 0 -> r1 < r2 -> r * r1 > r * r2


forall r r1 r2 : R,
r < 0 -> r1 < r2 -> r * r1 > r * r2

  
r, r1, r2:R
H:r < 0
H0:r1 < r2
- - r * r1 > - - r * r2

  
r, r1, r2:R
H:r < 0
H0:r1 < r2
- (- r * r1) > - (- r * r2)

  apply Ropp_lt_gt_contravar; auto with real.
Qed.

Cancellation

forall r r1 r2 : R,
0 < r -> r * r1 < r * r2 -> r1 < r2


forall r r1 r2 : R,
0 < r -> r * r1 < r * r2 -> r1 < r2

  
z, x, y:R
H:0 < z
H0:z * x < z * y
x < y

  
z, x, y:R
H:0 < z
H0:z * x < z * y
Eq0:x = y
x < y
z, x, y:R
H:0 < z
H0:z * x < z * y
Eq0:x > y
x < y

  
z, x, y:R
H:0 < z
H0:z * x < z * y
Eq0:x > y
x < y

  generalize (Rmult_lt_compat_l z y x H Eq0); intro; exfalso;
    generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1);
      intro; apply (Rlt_irrefl (z * x)); auto.
Qed.


forall r r1 r2 : R,
0 < r -> r1 * r < r2 * r -> r1 < r2


forall r r1 r2 : R,
0 < r -> r1 * r < r2 * r -> r1 < r2

  
r, r1, r2:R
H:0 < r
H0:r1 * r < r2 * r
r1 < r2

  
r, r1, r2:R
H:0 < r
H0:r1 * r < r2 * r
0 < r
r, r1, r2:R
H:0 < r
H0:r1 * r < r2 * r
r * r1 < r * r2

  
r, r1, r2:R
H:0 < r
H0:r1 * r < r2 * r
r * r1 < r * r2

  now rewrite 2!(Rmult_comm r).
Qed.


forall r r1 r2 : R,
0 < r -> r * r1 < r * r2 -> r1 < r2


forall r r1 r2 : R,
0 < r -> r * r1 < r * r2 -> r1 < r2
 eauto using Rmult_lt_reg_l with rorders. Qed.


forall r r1 r2 : R,
0 < r -> r * r1 <= r * r2 -> r1 <= r2


forall r r1 r2 : R,
0 < r -> r * r1 <= r * r2 -> r1 <= r2

  
z, x, y:R
H:0 < z
H0:z * x <= z * y
z * x < z * y -> x <= y
z, x, y:R
H:0 < z
H0:z * x <= z * y
z * x = z * y -> x <= y

  
z, x, y:R
H:0 < z
H0:z * x <= z * y
H1:z * x < z * y
x < y
z, x, y:R
H:0 < z
H0:z * x <= z * y
z * x = z * y -> x <= y

  
z, x, y:R
H:0 < z
H0:z * x <= z * y
z * x = z * y -> x <= y

  
z, x, y:R
H:0 < z
H0:z * x <= z * y
H1:z * x = z * y
/ z * (z * x) <= y
z, x, y:R
H:0 < z
H0:z * x <= z * y
H1:z * x = z * y
/ z * (z * x) = x

  
z, x, y:R
H:0 < z
H0:z * x <= z * y
H1:z * x = z * y
/ z * (z * x) <= / z * (z * y)
z, x, y:R
H:0 < z
H0:z * x <= z * y
H1:z * x = z * y
/ z * (z * y) = y
z, x, y:R
H:0 < z
H0:z * x <= z * y
H1:z * x = z * y
/ z * (z * x) = x

  
z, x, y:R
H:0 < z
H0:z * x <= z * y
H1:z * x = z * y
/ z * (z * y) = y
z, x, y:R
H:0 < z
H0:z * x <= z * y
H1:z * x = z * y
/ z * (z * x) = x

  
z, x, y:R
H:0 < z
H0:z * x <= z * y
H1:z * x = z * y
/ z * (z * x) = x

  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
Qed.


forall r r1 r2 : R,
0 < r -> r1 * r <= r2 * r -> r1 <= r2


forall r r1 r2 : R,
0 < r -> r1 * r <= r2 * r -> r1 <= r2

  
r, r1, r2:R
H:0 < r
H0:r1 * r <= r2 * r
r1 <= r2

  
r, r1, r2:R
H:0 < r
H0:r1 * r <= r2 * r
0 < r
r, r1, r2:R
H:0 < r
H0:r1 * r <= r2 * r
r * r1 <= r * r2

  
r, r1, r2:R
H:0 < r
H0:r1 * r <= r2 * r
r * r1 <= r * r2

  now rewrite 2!(Rmult_comm r).
Qed.

(*********************************************************)

Order and subtraction

(*********************************************************)


forall r1 r2 : R, r1 < r2 -> r1 - r2 < 0


forall r1 r2 : R, r1 < r2 -> r1 - r2 < 0

  
r1, r2:R
H:r1 < r2
r2 + (r1 - r2) < r2 + 0

  
r1, r2:R
H:r1 < r2
r1 < r2 + 0

  now rewrite Rplus_0_r.
Qed.
Hint Resolve Rlt_minus: real.


forall r1 r2 : R, r1 > r2 -> r1 - r2 > 0


forall r1 r2 : R, r1 > r2 -> r1 - r2 > 0

  
r1, r2:R
H:r1 > r2
r2 + 0 < r2 + (r1 - r2)

  
r1, r2:R
H:r1 > r2
r2 + 0 < r1

  now rewrite Rplus_0_r.
Qed.


forall a b : R, a < b -> 0 < b - a


forall a b : R, a < b -> 0 < b - a

  intros a b; apply Rgt_minus.
Qed.

(**********)

forall r1 r2 : R, r1 <= r2 -> r1 - r2 <= 0


forall r1 r2 : R, r1 <= r2 -> r1 - r2 <= 0

  destruct 1; unfold Rle; auto with real.
Qed.


forall r1 r2 : R, r1 >= r2 -> r1 - r2 >= 0


forall r1 r2 : R, r1 >= r2 -> r1 - r2 >= 0

  
r1, r2:R
H:r1 > r2
r1 - r2 >= 0
r1, r2:R
H:r1 = r2
r1 - r2 >= 0

    
r1, r2:R
H:r1 = r2
r1 - r2 >= 0

    right; auto using Rminus_diag_eq with rorders.
Qed.

(**********)

forall r1 r2 : R, r1 - r2 < 0 -> r1 < r2


forall r1 r2 : R, r1 - r2 < 0 -> r1 < r2

  
r1, r2:R
H:r1 - r2 < 0
r1 - r2 + r2 < r2
r1, r2:R
H:r1 - r2 < 0
r1 - r2 + r2 = r1

  
r1, r2:R
H:r1 - r2 < 0
r1 - r2 + r2 = r1

  ring.
Qed.


forall r1 r2 : R, r1 - r2 > 0 -> r1 > r2


forall r1 r2 : R, r1 - r2 > 0 -> r1 > r2

  
r1, r2:R
H:r1 - r2 > 0
r1 > 0 + r2

  
r1, r2:R
H:r1 - r2 > 0
r1 - r2 + r2 > 0 + r2
r1, r2:R
H:r1 - r2 > 0
r1 - r2 + r2 = r1

  
r1, r2:R
H:r1 - r2 > 0
r1 - r2 + r2 = r1

  ring.
Qed.


forall a b : R, 0 < b - a -> a < b


forall a b : R, 0 < b - a -> a < b
 intro; intro; apply Rminus_gt. Qed.

(**********)

forall r1 r2 : R, r1 - r2 <= 0 -> r1 <= r2


forall r1 r2 : R, r1 - r2 <= 0 -> r1 <= r2

  
r1, r2:R
H:r1 - r2 <= 0
r1 - r2 + r2 <= r2
r1, r2:R
H:r1 - r2 <= 0
r1 - r2 + r2 = r1

  
r1, r2:R
H:r1 - r2 <= 0
r1 - r2 + r2 = r1

  ring.
Qed.


forall r1 r2 : R, r1 - r2 >= 0 -> r1 >= r2


forall r1 r2 : R, r1 - r2 >= 0 -> r1 >= r2

  
r1, r2:R
H:r1 - r2 >= 0
r1 >= 0 + r2

  
r1, r2:R
H:r1 - r2 >= 0
r1 - r2 + r2 >= 0 + r2
r1, r2:R
H:r1 - r2 >= 0
r1 - r2 + r2 = r1

  
r1, r2:R
H:r1 - r2 >= 0
r1 - r2 + r2 = r1

  ring.
Qed.

(**********)

forall r s : R, 0 <= r -> 0 < s -> r + s <> 0


forall r s : R, 0 <= r -> 0 < s -> r + s <> 0

  
r, s:R
H:0 <= r
H0:0 < s
0 < r + s

  rewrite Rplus_comm; replace 0 with (0 + 0); auto with real.
Qed.
Hint Immediate tech_Rplus: real.

(*********************************************************)

Order and square function

(*********************************************************)


forall r : R, 0 <= r²


forall r : R, 0 <= r²

  
r:R
r0:r < 0
0 <= r * r
r:R
r0:0 <= r
0 <= r * r

  
r:R
r0:r < 0
0 <= - r * - r
r:R
r0:0 <= r
0 <= r * r

  
r:R
r0:0 <= r
0 <= r * r

  replace 0 with (0 * r); auto with real.
Qed.

(***********)

forall r : R, r <> 0 -> 0 < r²


forall r : R, r <> 0 -> 0 < r²

  
r:R
H:r <> 0
H0:r < 0
0 < r * r
r:R
H:r <> 0
H0:r > 0
0 < r * r

  
r:R
H:r <> 0
H0:r < 0
0 < - r * - r
r:R
H:r <> 0
H0:r > 0
0 < r * r

  
r:R
H:r <> 0
H0:r > 0
0 < r * r

  replace 0 with (0 * r); auto with real.
Qed.
Hint Resolve Rle_0_sqr Rlt_0_sqr: real.

(***********)

forall r1 r2 : R, r1² + r2² = 0 -> r1 = 0


forall r1 r2 : R, r1² + r2² = 0 -> r1 = 0

  intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b);
    auto with real.
Qed.


forall r1 r2 : R, r1² + r2² = 0 -> r1 = 0 /\ r2 = 0


forall r1 r2 : R, r1² + r2² = 0 -> r1 = 0 /\ r2 = 0

  
a, b:R
H:a² + b² = 0
a = 0
a, b:R
H:a² + b² = 0
b = 0

  
a, b:R
H:a² + b² = 0
b = 0

  
a, b:R
H:a² + b² = 0
b² + a² = 0

  rewrite Rplus_comm; auto with real.
Qed.

(*********************************************************)

Zero is less than one

(*********************************************************)


0 < 1


0 < 1

  
1² = 1

  unfold Rsqr; auto with real.
Qed.
Hint Resolve Rlt_0_1: real.


0 <= 1


0 <= 1

  
0 < 1

  exact Rlt_0_1.
Qed.

(*********************************************************)

Order and inverse

(*********************************************************)


forall r : R, 0 < r -> 0 < / r


forall r : R, 0 < r -> 0 < / r

  
r:R
H:0 < r
H0:/ r <= 0
False

  
r:R
H:0 < r
H0:/ r <= 0
1 <= 0

  
r:R
H:0 < r
H0:/ r <= 0
r * / r <= 0

  replace 0 with (r * 0); auto with real.
Qed.
Hint Resolve Rinv_0_lt_compat: real.

(*********)

forall r : R, r < 0 -> / r < 0


forall r : R, r < 0 -> / r < 0

  
r:R
H:r < 0
H0:0 <= / r
False

  
r:R
H:r < 0
H0:0 <= / r
1 <= 0

  
r:R
H:r < 0
H0:0 <= / r
r * / r <= 0

  replace 0 with (r * 0); auto with real.
Qed.
Hint Resolve Rinv_lt_0_compat: real.

(*********)

forall r1 r2 : R,
0 < r1 * r2 -> r1 < r2 -> / r2 < / r1


forall r1 r2 : R,
0 < r1 * r2 -> r1 < r2 -> / r2 < / r1

  
r1, r2:R
H:0 < r1 * r2
H0:r1 < r2
r1 * r2 * / r2 < r1 * r2 * / r1

  
r1, r2:R
H:0 < r1 * r2
H0:r1 < r2
H1:r1 <> 0
H2:r2 <> 0
r1 * r2 * / r2 < r1 * r2 * / r1

  
r1, r2:R
H:0 < r1 * r2
H0:r1 < r2
H1:r1 <> 0
H2:r2 <> 0
r1 < r1 * r2 * / r1
r1, r2:R
H:0 < r1 * r2
H0:r1 < r2
H1:r1 <> 0
H2:r2 <> 0
r1 = r1 * r2 * / r2

  
r1, r2:R
H:0 < r1 * r2
H0:r1 < r2
H1:r1 <> 0
H2:r2 <> 0
r2 = r1 * r2 * / r1
r1, r2:R
H:0 < r1 * r2
H0:r1 < r2
H1:r1 <> 0
H2:r2 <> 0
r1 = r1 * r2 * / r2

  
r1, r2:R
H:0 < r1 * r2
H0:r1 < r2
H1:r1 <> 0
H2:r2 <> 0
r1 = r1 * r2 * / r2

  symmetry ; auto with real.
Qed.


forall r1 r2 : R, 1 <= r1 -> r1 < r2 -> / r2 < / r1


forall r1 r2 : R, 1 <= r1 -> r1 < r2 -> / r2 < / r1

  
x, y:R
H':1 <= x
H'0:x < y
/ y < / x

  
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
/ y < / x

  
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
x * / y < x * / x

  
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
x * / y < 1

  
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
0 < y
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
y * (x * / y) < y * 1

  
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
y * (x * / y) < y * 1

  
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
y * (x * / y) = x -> y * (x * / y) < y * 1
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
y * (x * / y) = x

  
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
y * (x * / y) = x

  
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
y <> 0

  
x, y:R
H':1 <= x
H'0:x < y
Lt0:0 < x
y > 0

  red; apply Rlt_trans with (r2 := x); auto with real.
Qed.
Hint Resolve Rinv_1_lt_contravar: real.

(*********************************************************)

Miscellaneous

(*********************************************************)

(**********)

forall r : R, 0 <= r -> 0 < r + 1


forall r : R, 0 <= r -> 0 < r + 1

  
r:R
H:0 <= r
0 < r + 1

  
r:R
H:0 <= r
1 <= r + 1

  pattern 1 at 1; replace 1 with (0 + 1); auto with real.
Qed.
Hint Resolve Rle_lt_0_plus_1: real.

(**********)

forall r : R, r < r + 1


forall r : R, r < r + 1

  
r:R
r < r + 1

  pattern r at 1; replace r with (r + 0); auto with real.
Qed.
Hint Resolve Rlt_plus_1: real.

(**********)

forall r1 r2 : R, 0 < r2 -> r1 > r1 - r2


forall r1 r2 : R, 0 < r2 -> r1 > r1 - r2

  
r1, r2:R
H:0 < r2
r1 + - r2 < r1

  pattern r1 at 2; replace r1 with (r1 + 0); auto with real.
Qed.

(*********************************************************)

Injection from N to R

(*********************************************************)

(**********)

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


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

  intro; case n; auto with real.
Qed.

(**********)

forall n : nat, INR (1 + n) = INR 1 + INR n


forall n : nat, INR (1 + n) = INR 1 + INR n

  intro; simpl; case n; intros; auto with real.
Qed.

(**********)

forall n m : nat, INR (n + m) = INR n + INR m


forall n m : nat, INR (n + m) = INR n + INR m

  
m:nat
INR (0 + m) = INR 0 + INR m
n, m:nat
Hrecn:INR (n + m) = INR n + INR m
INR (S n + m) = INR (S n) + INR m

  
n, m:nat
Hrecn:INR (n + m) = INR n + INR m
INR (S n + m) = INR (S n) + INR m

  
n, m:nat
Hrecn:INR (n + m) = INR n + INR m
INR (S (n + m)) = INR (S n) + INR m

  
n, m:nat
Hrecn:INR (n + m) = INR n + INR m
INR (n + m) + 1 = INR n + 1 + INR m

  rewrite Hrecn; ring.
Qed.
Hint Resolve plus_INR: real.

(**********)

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


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

  
n, m:nat
le:(m <= n)%nat
forall p : nat, INR (p - 0) = INR p - INR 0
n, m:nat
le:(m <= n)%nat
forall p q : nat,
(p <= q)%nat ->
INR (q - p) = INR q - INR p ->
INR (S q - S p) = INR (S q) - INR (S p)

  
n, m:nat
le:(m <= n)%nat
forall p q : nat,
(p <= q)%nat ->
INR (q - p) = INR q - INR p ->
INR (S q - S p) = INR (S q) - INR (S p)

  
n, m:nat
le:(m <= n)%nat
p, q:nat
H:(p <= q)%nat
H0:INR (q - p) = INR q - INR p
INR (q - p) = INR q + 1 - (INR p + 1)

  rewrite H0; ring.
Qed.
Hint Resolve minus_INR: real.

(*********)

forall n m : nat, INR (n * m) = INR n * INR m


forall n m : nat, INR (n * m) = INR n * INR m

  
m:nat
INR (0 * m) = INR 0 * INR m
n, m:nat
Hrecn:INR (n * m) = INR n * INR m
INR (S n * m) = INR (S n) * INR m

  
n, m:nat
Hrecn:INR (n * m) = INR n * INR m
INR (S n * m) = INR (S n) * INR m

  
n, m:nat
Hrecn:INR (n * m) = INR n * INR m
INR (m + n * m) = (INR n + 1) * INR m

  rewrite plus_INR; rewrite Hrecn; ring.
Qed.
Hint Resolve mult_INR: real.


m, n:nat
INR (m ^ n) = pow (INR m) n


m, n:nat
INR (m ^ n) = pow (INR m) n
 now induction n as [|n IHn];[ | simpl; rewrite mult_INR, IHn]. Qed.

(*********)

forall n : nat, (0 < n)%nat -> 0 < INR n


forall n : nat, (0 < n)%nat -> 0 < INR n

  
n:nat
H:(0 < n)%nat
m:nat
H0:(1 <= m)%nat
H1:0 < INR m
0 < INR (S m)

  rewrite S_INR; auto with real.
Qed.
Hint Resolve lt_0_INR: real.


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


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

  
n, m:nat
H:(n < m)%nat
INR n < INR (S n)
n, m:nat
H:(n < m)%nat
m0:nat
H0:(S n <= m0)%nat
H1:INR n < INR m0
INR n < INR (S m0)

  
n, m:nat
H:(n < m)%nat
m0:nat
H0:(S n <= m0)%nat
H1:INR n < INR m0
INR n < INR (S m0)

  rewrite S_INR; apply Rlt_trans with (INR m0); auto with real.
Qed.
Hint Resolve lt_INR: real.


forall n : nat, (1 < n)%nat -> 1 < INR n


forall n : nat, (1 < n)%nat -> 1 < INR n

  apply lt_INR.
Qed.
Hint Resolve lt_1_INR: real.

(**********)

forall p : positive, 0 < INR (Pos.to_nat p)


forall p : positive, 0 < INR (Pos.to_nat p)

  
p:positive
(0 < Pos.to_nat p)%nat

  
p:positive
(0 < Pos.to_nat p)%nat

  apply Pos2Nat.is_pos.
Qed.
Hint Resolve pos_INR_nat_of_P: real.

(**********)

forall n : nat, 0 <= INR n


forall n : nat, 0 <= INR n

  
n:nat
0 <= INR 0
n:nat
forall n0 : nat, 0 <= INR (S n0)

  
n:nat
forall n0 : nat, 0 <= INR (S n0)

  auto with arith real.
Qed.
Hint Resolve pos_INR: real.


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


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

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

  
n:nat
H:INR n < INR 0
(n < 0)%nat
m:nat
IHm:forall n0 : nat, INR n0 < INR m -> (n0 < m)%nat
n:nat
H:INR n < INR (S m)
(n < S m)%nat

  
n:nat
H:INR n < INR 0
(n < 0)%nat
 
n:nat
H:INR n < INR 0
0 < 0

    
n:nat
H:INR n < INR 0
0 <= INR n

    apply pos_INR.
  
m:nat
IHm:forall n0 : nat, INR n0 < INR m -> (n0 < m)%nat
n:nat
H:INR n < INR (S m)
(n < S m)%nat
 
m:nat
IHm:forall n : nat, INR n < INR m -> (n < m)%nat
H:INR 0 < INR (S m)
(0 < S m)%nat
m:nat
IHm:forall n0 : nat, INR n0 < INR m -> (n0 < m)%nat
n:nat
H:INR (S n) < INR (S m)
(S n < S m)%nat

    
m:nat
IHm:forall n0 : nat, INR n0 < INR m -> (n0 < m)%nat
n:nat
H:INR (S n) < INR (S m)
(S n < S m)%nat

    
m:nat
IHm:forall n0 : nat, INR n0 < INR m -> (n0 < m)%nat
n:nat
H:INR (S n) < INR (S m)
INR n < INR m

    
m:nat
IHm:forall n0 : nat, INR n0 < INR m -> (n0 < m)%nat
n:nat
H:INR n + 1 < INR m + 1
INR n < INR m

    apply Rplus_lt_reg_r with (1 := H).
Qed.
Hint Resolve INR_lt: real.

(*********)

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


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

  
n, m:nat
H:(n <= m)%nat
m0:nat
H0:(n <= m0)%nat
H1:INR n <= INR m0
INR n <= INR (S m0)

  
n, m:nat
H:(n <= m)%nat
m0:nat
H0:(n <= m0)%nat
H1:INR n <= INR m0
INR n <= INR m0 + 1

  apply Rle_trans with (INR m0); auto with real.
Qed.
Hint Resolve le_INR: real.

(**********)

forall n : nat, INR n <> 0 -> n <> 0%nat


forall n : nat, INR n <> 0 -> n <> 0%nat

  
n:nat
H:INR n <> 0
H1:n = 0%nat
False

  
n:nat
H:INR n <> 0
H1:n = 0%nat
INR n = 0

  rewrite H1; trivial.
Qed.
Hint Immediate INR_not_0: real.

(**********)

forall n : nat, n <> 0%nat -> INR n <> 0


forall n : nat, n <> 0%nat -> INR n <> 0

  
n:nat
0%nat <> 0%nat -> INR 0 <> 0
n:nat
forall n0 : nat, S n0 <> 0%nat -> INR (S n0) <> 0

  
n:nat
forall n0 : nat, S n0 <> 0%nat -> INR (S n0) <> 0

  
n, n0:nat
H:S n0 <> 0%nat
INR n0 + 1 <> 0

  apply Rgt_not_eq; red; auto with real.
Qed.
Hint Resolve not_0_INR: real.


forall n m : nat, n <> m -> INR n <> INR m


forall n m : nat, n <> m -> INR n <> INR m

  
n, m:nat
H:n <> m
H1:(n <= m)%nat
INR n <> INR m
n, m:nat
H:n <> m
H1:(m < n)%nat
INR n <> INR m

  
n, m:nat
H:n <> m
H1:(n <= m)%nat
H2:(n < m)%nat
INR n <> INR m
n, m:nat
H:n <> m
H1:(n <= m)%nat
H2:n = m
INR n <> INR m
n, m:nat
H:n <> m
H1:(m < n)%nat
INR n <> INR m

  
n, m:nat
H:n <> m
H1:(n <= m)%nat
H2:n = m
INR n <> INR m
n, m:nat
H:n <> m
H1:(m < n)%nat
INR n <> INR m

  
n, m:nat
H:n <> m
H1:(m < n)%nat
INR n <> INR m

  apply not_eq_sym; apply Rlt_dichotomy_converse; auto with real.
Qed.
Hint Resolve not_INR: real.


forall n m : nat, INR n = INR m -> n = m


forall n m : nat, INR n = INR m -> n = m

  
n, m:nat
HR:INR n = INR m
n = m

  
n, m:nat
HR:INR n = INR m
H:n = m
n = m
n, m:nat
HR:INR n = INR m
H:n <> m
n = m

  
n, m:nat
HR:INR n = INR m
H:n <> m
n = m

  now apply not_INR in H.
Qed.
Hint Resolve INR_eq: real.


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


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

  
n, m:nat
H:INR n <= INR m
H0:INR n < INR m
(n <= m)%nat
n, m:nat
H:INR n <= INR m
H0:INR n = INR m
(n <= m)%nat

  
n, m:nat
H:INR n <= INR m
H0:INR n = INR m
(n <= m)%nat

  generalize (INR_eq n m H0); intro; rewrite H1; auto.
Qed.
Hint Resolve INR_le: real.


forall n : nat, n <> 1%nat -> INR n <> 1


forall n : nat, n <> 1%nat -> INR n <> 1

  
n:nat
n <> 1%nat -> INR n <> 1

  apply not_INR.
Qed.
Hint Resolve not_1_INR: real.

(*********************************************************)

Injection from Z to R

(*********************************************************)


(**********)

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


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

  intros z; idtac; apply Z_of_nat_complete; assumption.
Qed.


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


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

  
forall p : positive, 2 * INR (Pos.to_nat p) = IPR_2 p
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
forall p : positive, INR (Pos.to_nat p) = IPR p

    
p:positive
IHp:2 * INR (Pos.to_nat p) = IPR_2 p
2 * INR (Pos.to_nat p~1) = (R1 + R1) * (R1 + IPR_2 p)
p:positive
IHp:2 * INR (Pos.to_nat p) = IPR_2 p
2 * INR (Pos.to_nat p~0) = (R1 + R1) * IPR_2 p
2 * INR (Pos.to_nat 1) = R1 + R1
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
forall p : positive, INR (Pos.to_nat p) = IPR p

    
p:positive
IHp:2 * INR (Pos.to_nat p) = IPR_2 p
2 * (INR 2 * INR (Pos.to_nat p) + 1) =
(R1 + R1) * (R1 + 2 * INR (Pos.to_nat p))
p:positive
IHp:2 * INR (Pos.to_nat p) = IPR_2 p
2 * INR (Pos.to_nat p~0) = (R1 + R1) * IPR_2 p
2 * INR (Pos.to_nat 1) = R1 + R1
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
forall p : positive, INR (Pos.to_nat p) = IPR p

    
p:positive
IHp:2 * INR (Pos.to_nat p) = IPR_2 p
2 * INR (Pos.to_nat p~0) = (R1 + R1) * IPR_2 p
2 * INR (Pos.to_nat 1) = R1 + R1
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
forall p : positive, INR (Pos.to_nat p) = IPR p

    
2 * INR (Pos.to_nat 1) = R1 + R1
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
forall p : positive, INR (Pos.to_nat p) = IPR p

    
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
forall p : positive, INR (Pos.to_nat p) = IPR p

  
H:forall p0 : positive,
2 * INR (Pos.to_nat p0) = IPR_2 p0
p:positive
INR (Pos.to_nat p~1) = R1 + IPR_2 p
H:forall p0 : positive,
2 * INR (Pos.to_nat p0) = IPR_2 p0
p:positive
INR (Pos.to_nat p~0) = IPR_2 p
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
INR (Pos.to_nat 1) = R1

  
H:forall p0 : positive,
2 * INR (Pos.to_nat p0) = IPR_2 p0
p:positive
INR 2 * INR (Pos.to_nat p) + 1 =
R1 + 2 * INR (Pos.to_nat p)
H:forall p0 : positive,
2 * INR (Pos.to_nat p0) = IPR_2 p0
p:positive
INR (Pos.to_nat p~0) = IPR_2 p
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
INR (Pos.to_nat 1) = R1

  
H:forall p0 : positive,
2 * INR (Pos.to_nat p0) = IPR_2 p0
p:positive
INR (Pos.to_nat p~0) = IPR_2 p
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
INR (Pos.to_nat 1) = R1

  
H:forall p : positive,
2 * INR (Pos.to_nat p) = IPR_2 p
INR (Pos.to_nat 1) = R1

  easy.
Qed.

(**********)

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


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

  
INR 0 = IZR (Z.of_nat 0)
n:nat
INR (S n) = IZR (Z.of_nat (S n))

  
n:nat
INR (S n) = IZR (Z.of_nat (S n))

  
n:nat
INR (S n) = IZR (Z.pos (Pos.of_succ_nat n))
 
n:nat
INR (S n) = IPR (Pos.of_succ_nat n)

  now rewrite <- INR_IPR, SuccNat2Pos.id_succ.
Qed.


forall p q : positive,
IZR (Z.pos p + Z.neg q) =
IZR (Z.pos p) + IZR (Z.neg q)


forall p q : positive,
IZR (Z.pos p + Z.neg q) =
IZR (Z.pos p) + IZR (Z.neg q)

  
p, q:positive
IZR (Z.pos_sub p q) = IZR (Z.pos p) + IZR (Z.neg q)
 
p, q:positive
IZR
  match (p ?= q)%positive with
  | Eq => 0
  | Lt => Z.neg (q - p)
  | Gt => Z.pos (p - q)
  end = IZR (Z.pos p) + IZR (Z.neg q)

  
p, q:positive
H:p = q
R0 = IPR p + - IPR q
p, q:positive
H:(p < q)%positive
- IPR (q - p) = IPR p + - IPR q
p, q:positive
H:(q < p)%positive
IPR (p - q) = IPR p + - IPR q

  
q:positive
R0 = IPR q + - IPR q
p, q:positive
H:(p < q)%positive
- IPR (q - p) = IPR p + - IPR q
p, q:positive
H:(q < p)%positive
IPR (p - q) = IPR p + - IPR q
 
p, q:positive
H:(p < q)%positive
- IPR (q - p) = IPR p + - IPR q
p, q:positive
H:(q < p)%positive
IPR (p - q) = IPR p + - IPR q

  
p, q:positive
H:(p < q)%positive
- INR (Pos.to_nat q - Pos.to_nat p) =
INR (Pos.to_nat p) + - INR (Pos.to_nat q)
p, q:positive
H:(q < p)%positive
IPR (p - q) = IPR p + - IPR q

  
p, q:positive
H:(p < q)%positive
- (INR (Pos.to_nat q) - INR (Pos.to_nat p)) =
INR (Pos.to_nat p) + - INR (Pos.to_nat q)
p, q:positive
H:(q < p)%positive
IPR (p - q) = IPR p + - IPR q

  
p, q:positive
H:(q < p)%positive
IPR (p - q) = IPR p + - IPR q

  
p, q:positive
H:(q < p)%positive
INR (Pos.to_nat p - Pos.to_nat q) =
INR (Pos.to_nat p) + - INR (Pos.to_nat q)

  
p, q:positive
H:(q < p)%positive
INR (Pos.to_nat p) - INR (Pos.to_nat q) =
INR (Pos.to_nat p) + - INR (Pos.to_nat q)

  ring.
Qed.

(**********)

forall n m : Z, IZR (n + m) = IZR n + IZR m


forall n m : Z, IZR (n + m) = IZR n + IZR m

  
p, p0:positive
IZR (Z.pos p + Z.pos p0) =
IZR (Z.pos p) + IZR (Z.pos p0)
p, p0:positive
IZR (Z.pos p + Z.neg p0) =
IZR (Z.pos p) + IZR (Z.neg p0)
p, p0:positive
IZR (Z.neg p + Z.pos p0) =
IZR (Z.neg p) + IZR (Z.pos p0)
p, p0:positive
IZR (Z.neg p + Z.neg p0) =
IZR (Z.neg p) + IZR (Z.neg p0)

  
p, p0:positive
IZR (Z.pos (p + p0)) = IZR (Z.pos p) + IZR (Z.pos p0)
p, p0:positive
IZR (Z.pos p + Z.neg p0) =
IZR (Z.pos p) + IZR (Z.neg p0)
p, p0:positive
IZR (Z.neg p + Z.pos p0) =
IZR (Z.neg p) + IZR (Z.pos p0)
p, p0:positive
IZR (Z.neg p + Z.neg p0) =
IZR (Z.neg p) + IZR (Z.neg p0)
 
p, p0:positive
IPR (p + p0) = IPR p + IPR p0
p, p0:positive
IZR (Z.pos p + Z.neg p0) =
IZR (Z.pos p) + IZR (Z.neg p0)
p, p0:positive
IZR (Z.neg p + Z.pos p0) =
IZR (Z.neg p) + IZR (Z.pos p0)
p, p0:positive
IZR (Z.neg p + Z.neg p0) =
IZR (Z.neg p) + IZR (Z.neg p0)
 
p, p0:positive
INR (Pos.to_nat p + Pos.to_nat p0) =
INR (Pos.to_nat p) + INR (Pos.to_nat p0)
p, p0:positive
IZR (Z.pos p + Z.neg p0) =
IZR (Z.pos p) + IZR (Z.neg p0)
p, p0:positive
IZR (Z.neg p + Z.pos p0) =
IZR (Z.neg p) + IZR (Z.pos p0)
p, p0:positive
IZR (Z.neg p + Z.neg p0) =
IZR (Z.neg p) + IZR (Z.neg p0)
 
p, p0:positive
IZR (Z.pos p + Z.neg p0) =
IZR (Z.pos p) + IZR (Z.neg p0)
p, p0:positive
IZR (Z.neg p + Z.pos p0) =
IZR (Z.neg p) + IZR (Z.pos p0)
p, p0:positive
IZR (Z.neg p + Z.neg p0) =
IZR (Z.neg p) + IZR (Z.neg p0)

  
p, p0:positive
IZR (Z.neg p + Z.pos p0) =
IZR (Z.neg p) + IZR (Z.pos p0)
p, p0:positive
IZR (Z.neg p + Z.neg p0) =
IZR (Z.neg p) + IZR (Z.neg p0)

  
p, p0:positive
IZR (Z.neg p + Z.neg p0) =
IZR (Z.neg p) + IZR (Z.neg p0)

  
p, p0:positive
IZR (Z.neg (p + p0)) = IZR (Z.neg p) + IZR (Z.neg p0)
 
p, p0:positive
- IPR (p + p0) = - IPR p + - IPR p0
 
p, p0:positive
- (INR (Pos.to_nat p) + INR (Pos.to_nat p0)) =
- INR (Pos.to_nat p) + - INR (Pos.to_nat p0)

  apply Ropp_plus_distr.
Qed.

(**********)

forall n m : Z, IZR (n * m) = IZR n * IZR m


forall n m : Z, IZR (n * m) = IZR n * IZR m

  intros z t; case z; case t; simpl; auto with real;
    unfold IZR; intros m n; rewrite <- 3!INR_IPR, Pos2Nat.inj_mul, mult_INR; ring.
Qed.


forall (z : Z) (n : nat),
pow (IZR z) n = IZR (z ^ Z.of_nat n)


forall (z : Z) (n : nat),
pow (IZR z) n = IZR (z ^ Z.of_nat n)

 
z:Z
n:nat
IZR z * pow (IZR z) n =
IZR (Z.pow_pos z (Pos.of_succ_nat n))

 
z:Z
n:nat
IZR z * pow (IZR z) n =
IZR (Zpower_nat z (Pos.to_nat (Pos.of_succ_nat n)))

 
z:Z
n:nat
IZR z * pow (IZR z) n = IZR (Zpower_nat z (S n))
 
z:Z
n:nat
IZR z * pow (IZR z) n =
IZR
  (z *
   nat_rect (fun _ : nat => Z) 1%Z
     (fun _ : nat => Z.mul z) n)

 
z:Z
n:nat
IZR z * pow (IZR z) n =
IZR z *
IZR
  (nat_rect (fun _ : nat => Z) 1%Z
     (fun _ : nat => Z.mul z) n)

 
z:Z
n:nat
IHn:IZR z * pow (IZR z) n =
IZR z * IZR (nat_rect (fun _ : nat => Z) 1%Z (fun _ : nat => Z.mul z) n)
IZR z * (IZR z * pow (IZR z) n) =
IZR z *
IZR
  (z *
   nat_rect (fun _ : nat => Z) 1%Z
     (fun _ : nat => Z.mul z) n)

 rewrite mult_IZR;ring[IHn].
Qed.

(**********)

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


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

  intro; unfold Z.succ; apply plus_IZR.
Qed.

(**********)

forall n : Z, IZR (- n) = - IZR n


forall n : Z, IZR (- n) = - IZR n

  intros [|z|z]; unfold IZR; simpl; auto with real.
Qed.

Definition Ropp_Ropp_IZR := opp_IZR.


forall n m : Z, IZR (n - m) = IZR n - IZR m


forall n m : Z, IZR (n - m) = IZR n - IZR m

  
n, m:Z
IZR (n + - m) = IZR n + - IZR m

  
n, m:Z
IZR (n + - m) = IZR n + IZR (- m)

  apply plus_IZR.
Qed.

(**********)

forall n m : Z, IZR n - IZR m = IZR (n - m)


forall n m : Z, IZR n - IZR m = IZR (n - m)

  
z1, z2:Z
IZR z1 + - IZR z2 = IZR (z1 + - z2)

  rewrite <- (Ropp_Ropp_IZR z2); symmetry ; apply plus_IZR.
Qed.

(**********)

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


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

  
z:Z
H:0 < 0
(0 < 0)%Z
z:Z
p:positive
H:0 < IZR (Z.pos p)
(0 < Z.pos p)%Z
z:Z
p:positive
H:0 < IZR (Z.neg p)
(0 < Z.neg p)%Z

  
z:Z
p:positive
H:0 < IZR (Z.pos p)
(0 < Z.pos p)%Z
z:Z
p:positive
H:0 < IZR (Z.neg p)
(0 < Z.neg p)%Z

  
z:Z
p:positive
H:0 < IZR (Z.neg p)
(0 < Z.neg p)%Z

  
z:Z
p:positive
H:0 < IZR (Z.neg p)
IZR (Z.neg p) <= 0

  
z:Z
p:positive
H:0 < IZR (Z.neg p)
- IPR p <= R0

  
z:Z
p:positive
H:0 < IZR (Z.neg p)
- INR (Pos.to_nat p) <= R0

  auto with real.
Qed.

(**********)

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


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

  
z1, z2:Z
H:IZR z1 < IZR z2
(0 < z2 - z1)%Z

  
z1, z2:Z
H:IZR z1 < IZR z2
0 < IZR (z2 - z1)

  
z1, z2:Z
H:IZR z1 < IZR z2
0 < IZR z2 - IZR z1

  exact (Rgt_minus (IZR z2) (IZR z1) H).
Qed.

(**********)

forall n : Z, IZR n = 0 -> n = 0%Z


forall n : Z, IZR n = 0 -> n = 0%Z

  
p:positive
H:IZR (Z.pos p) = 0
Z.pos p = 0%Z
p:positive
H:IZR (Z.neg p) = 0
Z.neg p = 0%Z

  
p:positive
H:IZR (Z.pos p) = 0
IZR (Z.pos p) > 0
p:positive
H:IZR (Z.neg p) = 0
Z.neg p = 0%Z

  
p:positive
H:IZR (Z.pos p) = 0
IPR p > R0
p:positive
H:IZR (Z.neg p) = 0
Z.neg p = 0%Z
 
p:positive
H:IZR (Z.pos p) = 0
INR (Pos.to_nat p) > R0
p:positive
H:IZR (Z.neg p) = 0
Z.neg p = 0%Z

  
p:positive
H:IZR (Z.neg p) = 0
Z.neg p = 0%Z

  
p:positive
H:IZR (Z.neg p) = 0
IZR (Z.neg p) < 0

  
p:positive
H:IZR (Z.neg p) = 0
- IPR p < R0
 
p:positive
H:IZR (Z.neg p) = 0
- INR (Pos.to_nat p) < R0

  apply Ropp_lt_gt_0_contravar, lt_0_INR, Pos2Nat.is_pos.
Qed.

(**********)

forall n m : Z, IZR n = IZR m -> n = m


forall n m : Z, IZR n = IZR m -> n = m

  intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H);
    rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0);
      intro; omega.
Qed.

(**********)

forall n : Z, n <> 0%Z -> IZR n <> 0


forall n : Z, n <> 0%Z -> IZR n <> 0

  
z:Z
H:z <> 0%Z
H0:IZR z = 0
z = 0%Z

  apply eq_IZR; auto.
Qed.

(*********)

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


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

  
z:Z
H:0 < IZR z
(0 <= z)%Z
z:Z
H:0 = IZR z
(0 <= z)%Z

  
z:Z
H:0 = IZR z
(0 <= z)%Z

  rewrite (eq_IZR_R0 z); auto with zarith real.
Qed.

(**********)

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


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

  
z1, z2:Z
H:IZR z1 < IZR z2
(z1 <= z2)%Z
z1, z2:Z
H:IZR z1 = IZR z2
(z1 <= z2)%Z

  
z1, z2:Z
H:IZR z1 < IZR z2
(z1 < z2)%Z
z1, z2:Z
H:IZR z1 = IZR z2
(z1 <= z2)%Z

  
z1, z2:Z
H:IZR z1 = IZR z2
(z1 <= z2)%Z

  rewrite (eq_IZR z1 z2); auto with zarith real.
Qed.

(**********)

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


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

  
n:Z
IZR n <= 1 -> (n <= 1)%Z

  apply le_IZR.
Qed.

(**********)

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


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

  
m, n:Z
H:(m >= n)%Z
H0:IZR m < IZR n
False

  generalize (lt_IZR m n H0); intro; omega.
Qed.


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


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

  
m, n:Z
H:(m <= n)%Z
H0:IZR m > IZR n
False

  unfold Rgt in H0; generalize (lt_IZR n m H0); intro; omega.
Qed.


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


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

  
m, n:Z
H:(m < n)%Z
(m <= n)%Z -> IZR m < IZR n
m, n:Z
H:(m < n)%Z
(m <= n)%Z

  
m, n:Z
H:(m < n)%Z
H0:(m <= n)%Z
H1:IZR m = IZR n
IZR m < IZR n
m, n:Z
H:(m < n)%Z
(m <= n)%Z

  
m, n:Z
H:(m < n)%Z
(m <= n)%Z

  omega.
Qed.


forall z1 z2 : Z, z1 <> z2 -> IZR z1 <> IZR z2


forall z1 z2 : Z, z1 <> z2 -> IZR z1 <> IZR z2

intros; red; intro; elim H; apply eq_IZR; assumption.
Qed.

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.


forall n : Z, -1 < IZR n < 1 -> n = 0%Z


forall n : Z, -1 < IZR n < 1 -> n = 0%Z

  
z:Z
H1:-1 < IZR z
H2:IZR z < 1
z = 0%Z

  
z:Z
H1:-1 < IZR z
H2:IZR z < 1
(z <= 0)%Z
z:Z
H1:-1 < IZR z
H2:IZR z < 1
(0 <= z)%Z

  
z:Z
H1:-1 < IZR z
H2:IZR z < 1
(0 <= z)%Z

  
z:Z
H1:-1 < IZR z
H2:IZR z < 1
(Z.succ (-1) <= z)%Z

  apply Z.le_succ_l; apply lt_IZR; trivial.
Qed.


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


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

  
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
z = x

  
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
(z - x)%Z = 0%Z

  
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
-1 < IZR (z - x) < 1

  
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
-1 < IZR z - IZR x
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
IZR z - IZR x < 1

  
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
r - (r + 1) < IZR z - IZR x
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
r - (r + 1) = -1
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
IZR z - IZR x < 1

  
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
r - (r + 1) = -1
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
IZR z - IZR x < 1

  
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
IZR z - IZR x < 1

  
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
IZR z - IZR x < r + 1 - r
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
r + 1 - r = 1

  
r:R
z, x:Z
H1:r < IZR z
H2:IZR z <= r + 1
H3:r < IZR x
H4:IZR x <= r + 1
r + 1 - r = 1

  ring.
Qed.


(**********)

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


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

  intros; apply one_IZR_r_R1 with r; auto.
Qed.

(**********)

forall (r : R) (n : Z),
r < IZR n ->
IZR n <= r + 1 ->
(exists s : Z, s <> n /\ r < IZR s <= r + 1) -> False


forall (r : R) (n : Z),
r < IZR n ->
IZR n <= r + 1 ->
(exists s : Z, s <> n /\ r < IZR s <= r + 1) -> False

  
r:R
z:Z
H1:r < IZR z
H2:IZR z <= r + 1
s:Z
H3:s <> z
H4:r < IZR s
H5:IZR s <= r + 1
False

  apply H3; apply single_z_r_R1 with r; trivial.
Qed.

(*********)

forall r1 r2 : R, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2


forall r1 r2 : R, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2

  intros x y H H0; rewrite <- (Rmult_0_l x); rewrite <- (Rmult_comm x);
    apply (Rmult_le_compat_l x 0 y H H0).
Qed.


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


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

  
x, y:R
H1:0 < x
H2:x < y
/ y <= / x
x, y:R
H1:0 < x
H2:x = y
/ y <= / x

  
x, y:R
H1:0 < x
H2:x < y
/ y < / x
x, y:R
H1:0 < x
H2:x = y
/ y <= / x

  
x, y:R
H1:0 < x
H2:x < y
0 < x * y
x, y:R
H1:0 < x
H2:x = y
/ y <= / x

  
x, y:R
H1:0 < x
H2:x < y
0 < y
x, y:R
H1:0 < x
H2:x = y
/ y <= / x

  
x, y:R
H1:0 < x
H2:x = y
/ y <= / x

  
x, y:R
H1:0 < x
H2:x = y
/ y <= / y

  apply Rle_refl.
Qed.


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


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

  
x, y:R
H:0 < x
x <= y -> / y <= / x

  apply Rinv_le_contravar with (1 := H).
Qed.


forall x y : R, - x / y = - (x / y)

intros x y; unfold Rdiv; ring.
Qed.


forall r1 : R, 2 * r1 = r1 + r1


forall r1 : R, 2 * r1 = r1 + r1

  intro; ring.
Qed.


forall r1 : R, r1 = r1 / 2 + r1 / 2


forall r1 : R, r1 = r1 / 2 + r1 / 2

  
r1:R
2 <> 0

  now apply not_0_IZR.
Qed.


ring_morph 0 1 Rplus Rmult Rminus Ropp eq 0%Z 1%Z
  Z.add Z.mul Z.sub Z.opp Zeq_bool IZR


ring_morph 0 1 Rplus Rmult Rminus Ropp eq 0%Z 1%Z
  Z.add Z.mul Z.sub Z.opp Zeq_bool IZR


forall x y : Z, IZR (x + y) = IZR x + IZR y
forall x y : Z, IZR (x - y) = IZR x - IZR y
forall x y : Z, IZR (x * y) = IZR x * IZR y
forall x : Z, IZR (- x) = - IZR x
forall x y : Z, Zeq_bool x y = true -> IZR x = IZR y


forall x y : Z, IZR (x - y) = IZR x - IZR y
forall x y : Z, IZR (x * y) = IZR x * IZR y
forall x : Z, IZR (- x) = - IZR x
forall x y : Z, Zeq_bool x y = true -> IZR x = IZR y


forall x y : Z, IZR (x * y) = IZR x * IZR y
forall x : Z, IZR (- x) = - IZR x
forall x y : Z, Zeq_bool x y = true -> IZR x = IZR y


forall x : Z, IZR (- x) = - IZR x
forall x y : Z, Zeq_bool x y = true -> IZR x = IZR y


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


x, y:Z
H:Zeq_bool x y = true
IZR x = IZR y


x, y:Z
H:Zeq_bool x y = true
x = y

now apply Zeq_bool_eq.
Qed.


x, y:Z
IZR x = IZR y -> Zeq_bool x y = true


x, y:Z
IZR x = IZR y -> Zeq_bool x y = true


x, y:Z
H:IZR x = IZR y
Zeq_bool x y = true


x, y:Z
H:IZR x = IZR y
x = y

now apply eq_IZR.
Qed.

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 <=

(*********************************************************)


forall r1 r2 r3 r4 : R,
r3 >= 0 ->
r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4


forall r1 r2 r3 r4 : R,
r3 >= 0 ->
r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4

  intros; apply Rle_lt_trans with (r2 * r3); auto with real.
Qed.


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


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

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
x <= y

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:x <= y
x <= y
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
x <= y

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
x <= y

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
x + x <= y + x

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
x + x <= 2 * (y + (x - y) * / 2)

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
2 * x <= 2 * (y + (x - y) * / 2)

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
0 <= 2
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
x <= y + (x - y) * / 2

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
x <= y + (x - y) * / 2

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
0 < (x - y) * / 2

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
0 < x - y
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
0 < / 2

  
x, y:R
H:forall eps : R, 0 < eps -> x <= y + eps
H1:y < x
0 < / 2

  apply Rinv_0_lt_compat, Rlt_0_2.
Qed.

(**********)

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


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

  intros; elim (completeness E H H0); intros; split with x; assumption.
Qed.


forall a b : R, 0 < a -> 0 < b -> 0 < a / b


forall a b : R, 0 < a -> 0 < b -> 0 < a / b
 
intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption.
Qed.


forall a b c : R, (a + b) / c = a / c + b / c

intros a b c; apply Rmult_plus_distr_r.
Qed.


forall a b c : R, (a - b) / c = a / c - b / c

intros a b c; unfold Rminus, Rdiv; rewrite Rmult_plus_distr_r; ring.
Qed.

(* A test for equality function. *)

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


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

  
r1, r2:R
H:r1 < r2
{r1 = r2} + {r1 <> r2}
r1, r2:R
e:r1 = r2
{r1 = r2} + {r1 <> r2}
r1, r2:R
H:r1 > r2
{r1 = r2} + {r1 <> r2}

  
r1, r2:R
H:r1 < r2
{r1 = r2} + {r1 <> r2}
 right; red; intros ->; elim (Rlt_irrefl r2 H).
  
r1, r2:R
e:r1 = r2
{r1 = r2} + {r1 <> r2}
 left; assumption.
  
r1, r2:R
H:r1 > r2
{r1 = r2} + {r1 <> r2}
 right; red; intros ->; elim (Rlt_irrefl r2 H).
Qed.


(*********************************************************)

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