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

6 files changed, 6 insertions, 6 deletions

diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v
index 784e10455e..caf860af86 100644
--- a/theories/Arith/MinMax.v
+++ b/theories/Arith/MinMax.v
@@ -68,7 +68,7 @@ Lemma max_monotone: forall f,
 Proof. intros; apply max_monotone; auto. congruence. Qed.
 
 Lemma min_case_strong : forall n m (P:nat -> Type),
-  (m<=n -> P m) -> (n<=m -> P n) -> P (min n m).
+  (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
 Proof. intros; apply min_case_strong; auto. congruence. Defined.
 
 Lemma min_case : forall n m (P:nat -> Type),
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),
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),
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index ed9c035a15..49daacabda 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -303,7 +303,7 @@ Proof. intros. exact (MPRev.max_spec_le m n). Qed.
 
 Lemma min_case_strong : forall n m (P:O.t -> Type),
  (forall x y, x == y -> P x -> P y) ->
- (m<=n -> P m) -> (n<=m -> P n) -> P (min n m).
+ (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
 Proof. intros. apply (MPRev.max_case_strong m n P); auto. Qed.
 
 Lemma min_case : forall n m (P:O.t -> Type),
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index 5fa90487b0..e4d290ab2d 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -74,7 +74,7 @@ Lemma Zmax_monotone: forall f,
 Proof. intros; apply max_monotone; auto. congruence. Qed.
 
 Lemma Zmin_case_strong : forall n m (P:Z -> Type),
-  (m<=n -> P m) -> (n<=m -> P n) -> P (Zmin n m).
+  (n<=m -> P n) -> (m<=n -> P m) -> P (Zmin n m).
 Proof. intros; apply min_case_strong; auto. congruence. Defined.
 
 Lemma Zmin_case : forall n m (P:Z -> Type),