diff options
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Arith/Between.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index e6b4446017..1c08cdba37 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -126,8 +126,8 @@ Qed. Lemma in_int_exists : (k,l,r:nat)(in_int k l r)->(Q r)->(exists k l). Proof. -NewInduction 1; Intros. -Elim H1; Auto with arith. +NewDestruct 1; Intros. +Elim H0; Auto with arith. Qed. Lemma between_or_exists : |