From 6fe4d02936802bee35c73cdab2d08d8d4d3bd530 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 31 May 2002 21:04:33 +0000
Subject: Ajout d'occurrences de Field (ne pas enlever)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2742 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rbase.v | 17 ++++-------------
 1 file changed, 4 insertions(+), 13 deletions(-)

diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index d21fde297f..069ebe3cdc 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -531,8 +531,7 @@ Qed.
 
 (** Inverse *)
 Lemma Rinv_R1:``/1==1``.
-Apply (r_Rmult_mult ``1`` ``/1`` ``1``); Auto with real.
-Rewrite (Rinv_r R1 R1_neq_R0);Auto with real.
+Field;Auto with real.
 Qed.
 Hints Resolve Rinv_R1 : real.
 
@@ -545,26 +544,18 @@ Hints Resolve Rinv_neq_R0 : real.
 
 (*********)
 Lemma Rinv_Rinv:(r:R)``r<>0``->``/(/r)==r``.
-Intros;Apply (r_Rmult_mult ``/r``); Auto with real.
-Transitivity ``1``; Auto with real.
+Intros;Field;Auto with real.
 Qed.
 Hints Resolve Rinv_Rinv : real.
 
 (*********)
 Lemma Rinv_Rmult:(r1,r2:R)``r1<>0``->``r2<>0``->``/(r1*r2)==(/r1)*(/r2)``.
-Intros; Apply (r_Rmult_mult ``r1*r2``);Auto with real.
-Transitivity ``1``; Auto with real.
-Transitivity ``(r1*/r1)*(r2*(/r2))``; Auto with real.
-Rewrite Rinv_r; Trivial.
-Rewrite Rinv_r; Auto with real.
-Ring.
+Intros;Field;Auto with real.
 Qed.
 
 (*********)
 Lemma Ropp_Rinv:(r:R)``r<>0``->``-(/r)==/(-r)``.
-Intros; Apply (r_Rmult_mult ``-r``);Auto with real.
-Transitivity ``1``; Auto with real.
-Rewrite (Ropp_mul2 r ``/r``); Auto with real.
+Intros;Field;Auto with real.
 Qed.
 
 Lemma Rinv_r_simpl_r : (r1,r2:R)``r1<>0``->``r1*(/r1)*r2==r2``.
-- 
cgit v1.2.3