Imported Upstream version 8.5~beta1+dfsg

1 files changed, 11 insertions, 12 deletions

diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index cfc74fc4..c4e410ed 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -105,14 +105,14 @@ Proof.
   exists (x - IZR k0 * y).
   split.
   ring.
-  unfold k0; case (Rcase_abs y); intro.
+  unfold k0; case (Rcase_abs y) as [Hlt|Hge].
   assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl;
     unfold Rminus.
   replace (- ((1 + - IZR (up (x / - y))) * y)) with
     ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ].
   split.
   apply Rmult_le_reg_l with (/ - y).
-  apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact r.
+  apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact Hlt.
   rewrite Rmult_0_r; rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r;
     rewrite <- Ropp_inv_permute; [ idtac | assumption ].
   rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse;
@@ -125,14 +125,14 @@ Proof.
       (- (x * / y) + - (IZR (up (x * / - y)) - 1))) with 1;
     [ idtac | ring ].
   elim H0; intros _ H1; unfold Rdiv in H1; exact H1.
-  rewrite (Rabs_left _ r); apply Rmult_lt_reg_l with (/ - y).
-  apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact r.
+  rewrite (Rabs_left _ Hlt); apply Rmult_lt_reg_l with (/ - y).
+  apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact Hlt.
   rewrite <- Rinv_l_sym.
   rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r;
     rewrite <- Ropp_inv_permute; [ idtac | assumption ].
   rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse;
     rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ];
-      apply Rplus_lt_reg_r with (IZR (up (x / - y)) - 1).
+      apply Rplus_lt_reg_l with (IZR (up (x / - y)) - 1).
   replace (IZR (up (x / - y)) - 1 + 1) with (IZR (up (x / - y)));
     [ idtac | ring ].
   replace (IZR (up (x / - y)) - 1 + (- (x * / y) + - (IZR (up (x / - y)) - 1)))
@@ -157,22 +157,21 @@ Proof.
 	    (IZR (up (x * / y)) - x * / y + (x * / y + (1 - IZR (up (x * / y))))) with
 	    1; [ idtac | ring ]; elim H0; intros _ H2; unfold Rdiv in H2;
 	      exact H2.
-  rewrite (Rabs_right _ r); apply Rmult_lt_reg_l with (/ y).
+  rewrite (Rabs_right _ Hge); apply Rmult_lt_reg_l with (/ y).
   apply Rinv_0_lt_compat; assumption.
   rewrite <- (Rinv_l_sym _ H); rewrite (Rmult_comm (/ y));
     rewrite Rmult_plus_distr_r; rewrite Rmult_assoc; rewrite <- Rinv_r_sym;
       [ rewrite Rmult_1_r | assumption ];
-      apply Rplus_lt_reg_r with (IZR (up (x / y)) - 1);
+      apply Rplus_lt_reg_l with (IZR (up (x / y)) - 1);
 	replace (IZR (up (x / y)) - 1 + 1) with (IZR (up (x / y)));
 	  [ idtac | ring ];
 	  replace (IZR (up (x / y)) - 1 + (x * / y + (1 - IZR (up (x / y))))) with
 	    (x * / y); [ idtac | ring ]; elim H0; unfold Rdiv;
 	      intros H2 _; exact H2.
-  case (total_order_T 0 y); intro.
-  elim s; intro.
+  destruct (total_order_T 0 y) as [[Hlt|Heq]|Hgt].
   assumption.
-  elim H; symmetry ; exact b.
-  assert (H1 := Rge_le _ _ r); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 r0)).
+  elim H; symmetry ; exact Heq.
+  apply Rge_le in Hge; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hge Hgt)).
 Qed.
 
 Lemma tech8 : forall n i:nat, (n <= S n + i)%nat.