From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/QArith/Qreals.v | 44 +++++++++++++++++++-------------------------
 1 file changed, 19 insertions(+), 25 deletions(-)

(limited to 'theories/QArith/Qreals.v')

diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 048e409c..c8329625 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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)         *)
 (************************************************************************)
 
 Require Export Rbase.
@@ -15,7 +17,8 @@ Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R.
 
 Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R.
 Proof.
-intros; apply not_O_IZR; auto with qarith.
+intros.
+now apply not_O_IZR.
 Qed.
 
 Hint Resolve IZR_nz Rmult_integral_contrapositive.
@@ -48,8 +51,7 @@ assert ((X1 * Y2)%R = (Y1 * X2)%R).
  apply IZR_eq; auto.
 clear H.
 field_simplify_eq; auto.
-ring_simplify X1 Y2 (Y2 * X1)%R.
-rewrite H0;  ring.
+rewrite H0; ring.
 Qed.
 
 Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y.
@@ -66,10 +68,8 @@ replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto).
 replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto).
 apply Rmult_le_compat_r; auto.
 apply Rmult_le_pos.
-unfold X2; replace 0%R with (IZR 0); auto; apply IZR_le;
- auto with zarith.
-unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_le;
- auto with zarith.
+now apply IZR_le.
+now apply IZR_le.
 Qed.
 
 Lemma Qle_Rle : forall x y : Q, x<=y -> (Q2R x <= Q2R y)%R.
@@ -88,10 +88,8 @@ replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto).
 replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto).
 apply Rmult_le_compat_r; auto.
 apply Rmult_le_pos; apply Rlt_le; apply Rinv_0_lt_compat.
-unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
- auto with zarith.
-unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
- auto with zarith.
+now apply IZR_lt.
+now apply IZR_lt.
 Qed.
 
 Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x<y.
@@ -108,10 +106,8 @@ replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto).
 replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto).
 apply Rmult_lt_compat_r; auto.
 apply Rmult_lt_0_compat.
-unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
- auto with zarith.
-unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
- auto with zarith.
+now apply IZR_lt.
+now apply IZR_lt.
 Qed.
 
 Lemma Qlt_Rlt : forall x y : Q, x<y -> (Q2R x < Q2R y)%R.
@@ -130,10 +126,8 @@ replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto).
 replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto).
 apply Rmult_lt_compat_r; auto.
 apply Rmult_lt_0_compat; apply Rinv_0_lt_compat.
-unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
- auto with zarith.
-unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red;
- auto with zarith.
+now apply IZR_lt.
+now apply IZR_lt.
 Qed.
 
 Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R.
@@ -173,8 +167,8 @@ unfold Qinv, Q2R, Qeq; intros (x1, x2). case x1; unfold Qnum, Qden.
 simpl; intros; elim H; trivial.
 intros; field; auto. 
 intros;
-  change (IZR (Zneg x2)) with (- IZR (' x2))%R;
-  change (IZR (Zneg p)) with (- IZR (' p))%R;
+  change (IZR (Zneg x2)) with (- IZR (Zpos x2))%R;
+  change (IZR (Zneg p)) with (- IZR (Zpos p))%R;
   simpl; field; (*auto 8 with real.*)
   repeat split; auto; auto with real.
 Qed.
-- 
cgit v1.2.3