From 78c1f8921ccbbdf6c7114ae8519e6a860f99ec6f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Nov 2003 10:03:31 +0000
Subject: Utilisation du total_order non constructif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5019 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rbasic_fun.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index fb164fde6e..c586acdca0 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -410,11 +410,10 @@ Qed.
 (* ||a|-|b||<=|a-b| *)
 Lemma Rabsolu_triang_inv2 : (a,b:R) ``(Rabsolu ((Rabsolu a)-(Rabsolu b)))<=(Rabsolu (a-b))``. 
 Cut (a,b:R) ``(Rabsolu b)<=(Rabsolu a)``->``(Rabsolu ((Rabsolu a)-(Rabsolu b))) <= (Rabsolu (a-b))``. 
-Intros; Case (total_order_T (Rabsolu a) (Rabsolu b)); Intro. 
-Elim s; Intro. 
+Intros; NewDestruct (total_order (Rabsolu a) (Rabsolu b)) as [Hlt|[Heq|Hgt]].
 Rewrite <- (Rabsolu_Ropp ``(Rabsolu a)-(Rabsolu b)``); Rewrite <- (Rabsolu_Ropp ``a-b``); Do 2 Rewrite Ropp_distr2. 
 Apply H; Left; Assumption. 
-Rewrite b0; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply Rabsolu_pos. 
+Rewrite Heq; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Apply Rabsolu_pos. 
 Apply H; Left; Assumption. 
 Intros; Replace ``(Rabsolu ((Rabsolu a)-(Rabsolu b)))`` with ``(Rabsolu a)-(Rabsolu b)``. 
 Apply Rabsolu_triang_inv. 
-- 
cgit v1.2.3