diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/Nminmax.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Pminmax.v | 2 |
2 files changed, 2 insertions, 2 deletions
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), |