From 854948d1ebf547ee60414b73e0be1a7827c6d1c8 Mon Sep 17 00:00:00 2001
From: desmettr
Date: Wed, 9 Oct 2002 09:21:38 +0000
Subject: MAJ pour modification dans Rcomplet

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3107 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rsqrt_def.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index d09b377ae3..948d166105 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -430,7 +430,7 @@ Cut (n:nat)``0<=(f (Wn n))``.
 Intros.
 Assert H9 := (H6 H8).
 Assert H10 := (H5 H7).
-Apply Rle_Rle_eq; Assumption.
+Apply Rle_antisym; Assumption.
 Intro.
 Unfold Wn.
 Cut (z:R) (cond_pos z)=true <-> ``0<=z``.
-- 
cgit v1.2.3