From d1f2e143ff56e53d6feee4158bc9f69b8d3e9ee1 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 17 Dec 2009 16:46:56 +0000
Subject: Reverse order of arguments in min_case_strong for better uniformity
 (and compatibility...)

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

(limited to 'theories/Reals')

diff --git a/theories/Reals/Rminmax.v b/theories/Reals/Rminmax.v
index 70bc00c9f5..e78e895423 100644
--- a/theories/Reals/Rminmax.v
+++ b/theories/Reals/Rminmax.v
@@ -59,7 +59,7 @@ Lemma Rmax_monotone: forall f,
 Proof. intros; apply max_monotone; auto. congruence. Qed.
 
 Lemma Rmin_case_strong : forall n m (P:R -> Type),
-  (m<=n -> P m) -> (n<=m -> P n) -> P (Rmin n m).
+  (n<=m -> P n) -> (m<=n -> P m) -> P (Rmin n m).
 Proof. intros; apply min_case_strong; auto. congruence. Defined.
 
 Lemma Rmin_case : forall n m (P:R -> Type),
-- 
cgit v1.2.3