diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-28 19:35:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-28 19:35:03 +0000 |
| commit | 1c4a4908a82e2eba9cc2d335697d51182f7314c2 (patch) | |
| tree | 39f6a5b7caf7d583af468d59c9f62378a748f8d3 /theories/ZArith/Zorder.v | |
| parent | be76b6af359ea61bc71e59efb4802ff01cce728c (diff) | |
Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12888 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zorder.v')
| -rw-r--r-- | theories/ZArith/Zorder.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index aad90a1e8..511c364bc 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 ]. |