diff options
| -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 8a62eb88ba..a3b102055c 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. |