From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 theories/QArith/Qreals.v | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

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

diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 5b7480c1..6bd161f3 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -6,12 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qreals.v 8883 2006-05-31 21:56:37Z letouzey $ i*)
+(*i $Id: Qreals.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Export Rbase.
 Require Export QArith_base.
 
-(** * A field tactic for rational numbers. *)
+(** A field tactic for rational numbers. *)
 
 (** Since field cannot operate on setoid datatypes (yet?), 
   we translate Q goals into reals before applying field. *)
@@ -52,8 +52,9 @@ assert ((X1 * Y2)%R = (Y1 * X2)%R).
  unfold X1, X2, Y1, Y2 in |- *; do 2 rewrite <- mult_IZR.
  apply IZR_eq; auto.
 clear H.
-field; auto.
-rewrite <- H0; field; auto.
+field_simplify_eq; auto.
+ring_simplify X1 Y2 (Y2 * X1)%R.
+rewrite H0 in |- *;  ring.
 Qed.
 
 Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y.
@@ -176,16 +177,11 @@ unfold Qinv, Q2R, Qeq in |- *; intros (x1, x2); unfold Qden, Qnum in |- *.
 case x1.
 simpl in |- *; intros; elim H; trivial.
 intros; field; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rinv_neq_0_compat; auto.
-intros; field; auto.
-do 2 rewrite <- mult_IZR.
-simpl in |- *; rewrite Pmult_comm; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply Rmult_integral_contrapositive; split; auto.
-apply not_O_IZR; auto with qarith.
-apply Rinv_neq_0_compat; auto.
+intros; 
+  change (IZR (Zneg x2)) with (- IZR (' x2))%R in |- *;
+  change (IZR (Zneg p)) with (- IZR (' p))%R in |- *;
+  field; (*auto 8 with real.*)
+  repeat split; auto; auto with real.
 Qed.
 
 Lemma Q2R_div :
@@ -210,4 +206,4 @@ Goal forall x y : Q, ~ y==0#1 -> (x/y)*y == x.
 intros; QField.
 intro; apply H; apply eqR_Qeq.
 rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real.
-Abort.
\ No newline at end of file
+Abort.
-- 
cgit v1.2.3