diff options
author | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-05 19:22:22 +0000 |
---|---|---|
committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-05 19:22:22 +0000 |
commit | 49623ae29421c2ccd16f82d71b65cfacd0877fec (patch) | |
tree | 5d9135d01882033f9df993e088fb287895b7954c /theories/Arith | |
parent | 737faa34acc0858b7c8f766a20b1d0bcedbf36c7 (diff) |
Backtrack sur la révision #10401 : suppression de le_minus de la base de hints arith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10621 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith')
-rw-r--r-- | theories/Arith/Minus.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 8a62eb88b..a3b102055 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -124,12 +124,11 @@ Corollary le_minus : forall n m, n - m <= n. Proof. intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith. Qed. -Hint Resolve le_minus: arith v62. Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n. Proof. intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *; - auto with arith. + auto using le_minus with arith. intros; absurd (0 < 0); auto with arith. Qed. Hint Resolve lt_minus: arith v62. |