diff options
Diffstat (limited to 'theories/Arith/Between.v')
| -rwxr-xr-x | theories/Arith/Between.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 2d5104af26..14b2453358 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -42,7 +42,7 @@ Lemma between_Sk_l : (k,l:nat)(between k l)->(le (S k) l)->(between (S k) l). Proof. NewInduction 1. Intros; Absurd (le (S k) k); Auto with arith. -Induction H; Auto with arith. +NewDestruct H; Auto with arith. Qed. Hints Resolve between_Sk_l : arith v62. |