diff options
| author |  emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-08 17:06:32 +0000 |
|---|---|---|
| committer | emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-08 17:06:32 +0000 |
| commit | 8a51418e76da874843d6b58b6615dc12a82e2c0a (patch) | |
| tree | 237cd1a934d3a24f1d954e7400e5a683476deb23 /theories/Numbers/NatInt | |
| parent | c08b8247aec05b34a908663aa160fdbd617b8220 (diff) | |
Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10304 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 854542906..4ded2b892 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -116,7 +116,10 @@ Qed. Theorem NZlt_le_succ : forall n m : NZ, n < m <-> S n <= m. Proof. intro n; NZinduct m n. -rewrite_false (n < n) NZlt_irrefl. now rewrite_false (S n <= n) NZnle_succ_l. +setoid_replace (n < n) with False using relation iff by + (apply -> neg_false; apply NZlt_irrefl). +now setoid_replace (S n <= n) with False using relation iff by + (apply -> neg_false; apply NZnle_succ_l). intro m. rewrite NZlt_succ_le. rewrite NZle_succ_le_or_eq_succ. rewrite NZsucc_inj_wd. rewrite (NZle_lt_or_eq n m). rewrite or_cancel_r. |