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/NArith/Nminmax.v | 2 +-
 theories/NArith/Pminmax.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'theories/NArith')

diff --git a/theories/NArith/Nminmax.v b/theories/NArith/Nminmax.v
index 86e6b609fd..c2fee9c7e3 100644
--- a/theories/NArith/Nminmax.v
+++ b/theories/NArith/Nminmax.v
@@ -61,7 +61,7 @@ Lemma Nmax_monotone: forall f,
 Proof. intros; apply max_monotone; auto. congruence. Qed.
 
 Lemma Nmin_case_strong : forall n m (P:N -> Type),
-  (m<=n -> P m) -> (n<=m -> P n) -> P (Nmin n m).
+  (n<=m -> P n) -> (m<=n -> P m) -> P (Nmin n m).
 Proof. intros; apply min_case_strong; auto. congruence. Defined.
 
 Lemma Nmin_case : forall n m (P:N -> Type),
diff --git a/theories/NArith/Pminmax.v b/theories/NArith/Pminmax.v
index 18008d18d0..afae63f5a4 100644
--- a/theories/NArith/Pminmax.v
+++ b/theories/NArith/Pminmax.v
@@ -61,7 +61,7 @@ Lemma Pmax_monotone: forall f,
 Proof. intros; apply max_monotone; auto. congruence. Qed.
 
 Lemma Pmin_case_strong : forall n m (P:positive -> Type),
-  (m<=n -> P m) -> (n<=m -> P n) -> P (Pmin n m).
+  (n<=m -> P n) -> (m<=n -> P m) -> P (Pmin n m).
 Proof. intros; apply min_case_strong; auto. congruence. Defined.
 
 Lemma Pmin_case : forall n m (P:positive -> Type),
-- 
cgit v1.2.3