From e0ff9328c51cec3bd65d4893af5da5c9f8ba2570 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 3 Dec 2013 13:40:51 +0100
Subject: Remove a useless hypothesis from Rle_Rinv.

---
 theories/Reals/Exp_prop.v   |  6 ++----
 theories/Reals/RIneq.v      | 24 ++++++++++++++----------
 theories/Reals/Ratan.v      |  6 ++----
 theories/Reals/RiemannInt.v |  6 ++----
 4 files changed, 20 insertions(+), 22 deletions(-)

diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index b65ab045b3..40064fd511 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -173,8 +173,7 @@ Proof.
   apply pow_le; apply Rabs_pos.
   rewrite (Rmult_comm (/ INR (fact (S n0)))); apply Rmult_le_compat_l.
   apply pow_le; apply Rabs_pos.
-  apply Rle_Rinv.
-  apply INR_fact_lt_0.
+  apply Rinv_le_contravar.
   apply INR_fact_lt_0.
   apply le_INR; apply fact_le; apply le_n_S.
   apply le_plus_l.
@@ -254,8 +253,7 @@ Proof.
   do 2 rewrite <- (Rmult_comm (/ INR (fact (N - n0)))).
   apply Rmult_le_compat_l.
   left; apply Rinv_0_lt_compat; apply INR_fact_lt_0.
-  apply Rle_Rinv.
-  apply INR_fact_lt_0.
+  apply Rinv_le_contravar.
   apply INR_fact_lt_0.
   apply le_INR.
   apply fact_le.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index bfa975aaba..3adea5a10d 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1935,18 +1935,22 @@ Proof.
     apply (Rmult_le_compat_l x 0 y H H0).
 Qed.
 
+Lemma Rinv_le_contravar :
+  forall x y, 0 < x -> x <= y -> / y <= / x.
+Proof.
+  intros x y H1 [H2|H2].
+  apply Rlt_le.
+  apply Rinv_lt_contravar with (2 := H2).
+  apply Rmult_lt_0_compat with (1 := H1).
+  now apply Rlt_trans with x.
+  rewrite H2.
+  apply Rle_refl.
+Qed.
+
 Lemma Rle_Rinv : forall x y:R, 0 < x -> 0 < y -> x <= y -> / y <= / x.
 Proof.
-  intros; apply Rmult_le_reg_l with x.
-  apply H.
-  rewrite <- Rinv_r_sym.
-  apply Rmult_le_reg_l with y.
-  apply H0.
-  rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc;
-    rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; apply H1.
-  red; intro; rewrite H2 in H0; elim (Rlt_irrefl _ H0).
-  red; intro; rewrite H2 in H; elim (Rlt_irrefl _ H).
+  intros x y H _.
+  apply Rinv_le_contravar with (1 := H).
 Qed.
 
 Lemma double : forall r1, 2 * r1 = r1 + r1.
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index 1a0ea969e1..b1eb17b212 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -810,13 +810,11 @@ intros x Hx eps Heps.
    apply Rle_lt_trans with (/ INR (2 * N + 1))%R.
    unfold Rdiv.
    rewrite Rmult_1_l.
-   apply Rle_Rinv.
+   apply Rinv_le_contravar.
    apply lt_INR_0.
    omega.
-   replace 0 with (INR 0) by intuition.
-   apply lt_INR.
+   apply le_INR.
    omega.
-   intuition.
    rewrite <- (Rinv_involutive eps).
    apply Rinv_lt_contravar.
    apply Rmult_lt_0_compat.
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 0a00ca2237..3fe3694f9b 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -388,11 +388,9 @@ Proof.
     [ idtac
       | left; change (0 < / (INR n + 1)); apply Rinv_0_lt_compat;
         assumption ]; apply Rle_lt_trans with (/ (INR x + 1)).
-  apply Rle_Rinv.
+  apply Rinv_le_contravar.
   apply Rplus_le_lt_0_compat; [ apply pos_INR | apply Rlt_0_1 ].
-  assumption.
-  do 2 rewrite <- (Rplus_comm 1); apply Rplus_le_compat_l; apply le_INR;
-    apply H4.
+  apply Rplus_le_compat_r; apply le_INR; apply H4.
   rewrite <- (Rinv_involutive eps).
   apply Rinv_lt_contravar.
   apply Rmult_lt_0_compat.
-- 
cgit v1.2.3