From 3fe1b36a59fe6b20f94c188eb01c9b07368da3af Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 May 2006 09:26:36 +0000
Subject: MAJ suite placement automatiquement de Rlist au niveau prédicatif le
 plus bas, i.e. Set; renommage canonique Rmax_comm

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

diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 2785b21122..723de4d406 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -107,11 +107,13 @@ Lemma RmaxLess2 : forall r1 r2, r2 <= Rmax r1 r2.
 intros r1 r2; unfold Rmax in |- *; case (Rle_dec r1 r2); auto with real.
 Qed.
  
-Lemma RmaxSym : forall p q:R, Rmax p q = Rmax q p.
+Lemma Rmax_comm : forall p q:R, Rmax p q = Rmax q p.
 intros p q; unfold Rmax in |- *; case (Rle_dec p q); case (Rle_dec q p); auto;
  intros H1 H2; apply Rle_antisym; auto with real.
 Qed.
 
+Notation RmaxSym := Rmax_comm (only parsing).
+
 Lemma RmaxRmult :
  forall (p q:R) r, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p q.
 intros p q r H; unfold Rmax in |- *.
@@ -467,4 +469,4 @@ intros p0; apply Rabs_right; auto with real zarith.
 intros p0; rewrite Rabs_Ropp.
 apply Rabs_right; auto with real zarith.
 Qed.
- 
\ No newline at end of file
+ 
-- 
cgit v1.2.3