From d1f49a3d69a300620b016bd7f3857111f3b51567 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Thu, 16 Jan 2003 17:13:43 +0000
Subject: Ajout de RCompute

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3514 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/DiscrR.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index f7e3e0b1f4..2d8d0476a1 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -69,4 +69,10 @@ Recursive Tactic Definition Sup :=
   | [ |- (Rlt (Ropp ?1) (Ropp ?2)) ] -> Apply Rlt_Ropp; Sup
   | [ |- (Rlt (Ropp ?1) ?2) ] -> Apply Rlt_trans with ``0``; Sup
   | [ |- (Rlt ?1 ?2) ] -> SupOmega
-  | _ -> Idtac.
\ No newline at end of file
+  | _ -> Idtac.
+
+Lemma IZR_eq : (z1,z2:Z) z1=z2 -> (IZR z1)==(IZR z2).
+Intros; Rewrite H; Reflexivity.
+Qed.
+
+Tactic Definition RCompute := Replace R1 with (IZR `1`); [Replace R0 with (IZR `0`); [Repeat Rewrite <- plus_IZR Orelse Rewrite <- mult_IZR Orelse Rewrite <- Ropp_Ropp_IZR Orelse Rewrite Z_R_minus; Apply IZR_eq; Ring | Reflexivity] | Reflexivity].
-- 
cgit v1.2.3