diff options
| author | msozeau | 2008-03-07 16:32:12 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-07 16:32:12 +0000 |
| commit | ec850ff623801e514b3ed0a42beb6f7984992520 (patch) | |
| tree | 6a03dd3d0545b927326f28e7d8da08a850cead5f /theories/Numbers/NatInt/NZOrder.v | |
| parent | 905c47d6a07cc69b9e7aa0b9d73caeacf2b1d2be (diff) | |
Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part
of the fix I added an optional "by" annotation for rewrite to solve said
conditions in the same tactic call. Most of the theories have been
updated, only FSets is missing, Pierre will take care of it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NatInt/NZOrder.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index bc3600f9ce..133bbde4df 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -140,11 +140,12 @@ setoid_replace (n < n) with False using relation iff by now setoid_replace (S n <= n) with False using relation iff by (apply -> neg_false; apply NZnle_succ_diag_l). intro m. rewrite NZlt_succ_r. rewrite NZle_succ_r. -rewrite NZsucc_inj_wd. rewrite (NZlt_eq_cases n m). +rewrite NZsucc_inj_wd. +rewrite (NZlt_eq_cases n m). rewrite or_cancel_r. +reflexivity. intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l. apply NZlt_neq. -reflexivity. Qed. Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m. |