diff options
| -rw-r--r-- | theories/Arith/MinMax.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Nminmax.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Pminmax.v | 2 | ||||
| -rw-r--r-- | theories/Reals/Rminmax.v | 2 | ||||
| -rw-r--r-- | theories/Structures/GenericMinMax.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zminmax.v | 2 |
6 files changed, 6 insertions, 6 deletions
diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v index 784e10455..caf860af8 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 86e6b609f..c2fee9c7e 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 18008d18d..afae63f5a 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 70bc00c9f..e78e89542 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 ed9c035a1..49daacabd 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 5fa90487b..e4d290ab2 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), |