diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | theories/ZArith/Znat.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zorder.v | 6 |
3 files changed, 6 insertions, 4 deletions
@@ -155,6 +155,8 @@ Library - Lemmas in library Relations and Reals have been homogenized a bit. - The implicit argument of Logic.eq is now maximally inserted, allowing to simply write "eq" instead of "@eq _" in morphism signatures. +- Wrongly named lemmas (Zlt_gt_succ and Zlt_succ_gt) fixed (potential source + of incompatibilities) - List library: - Definitions of list, length and app are now in Init/Datatypes. Support for compatibility is provided. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 0fc27e38bd..dfd9b54506 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -91,7 +91,7 @@ Qed. Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m. Proof. - intros x y H; apply Zgt_lt; apply Zlt_succ_gt; rewrite <- inj_S; apply inj_le; + intros x y H; apply Zgt_lt; apply Zle_succ_gt; rewrite <- inj_S; apply inj_le; exact H. Qed. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index aad90a1e8c..511c364bc7 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -413,7 +413,7 @@ Proof. | elim (Zcompare_Gt_Lt_antisym (n + 1) p); intros H4 H5; apply H4; exact H3 ]. Qed. -Lemma Zlt_gt_succ : forall n m:Z, n <= m -> Zsucc m > n. +Lemma Zle_gt_succ : forall n m:Z, n <= m -> Zsucc m > n. Proof. intros n p H; apply Zgt_le_trans with p. apply Zgt_succ. @@ -422,7 +422,7 @@ Qed. Lemma Zle_lt_succ : forall n m:Z, n <= m -> n < Zsucc m. Proof. - intros n m H; apply Zgt_lt; apply Zlt_gt_succ; assumption. + intros n m H; apply Zgt_lt; apply Zle_gt_succ; assumption. Qed. Lemma Zlt_le_succ : forall n m:Z, n < m -> Zsucc n <= m. @@ -440,7 +440,7 @@ Proof. intros n m H; apply Zgt_succ_le; apply Zlt_gt; assumption. Qed. -Lemma Zlt_succ_gt : forall n m:Z, Zsucc n <= m -> m > n. +Lemma Zle_succ_gt : forall n m:Z, Zsucc n <= m -> m > n. Proof. intros n m H; apply Zle_gt_trans with (m := Zsucc n); [ assumption | apply Zgt_succ ]. |