aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/ZUtil.v')
-rw-r--r--src/Util/ZUtil.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index fe329d3f9..a8b18ffef 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -812,7 +812,7 @@ Proof.
assert (Hn : -X <= a - b) by lia.
assert (Hp : a - b <= X - 1) by lia.
split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ];
- autorewrite with zsimplify; reflexivity.
+ instantiate; autorewrite with zsimplify; try reflexivity.
Qed.
Hint Resolve (fun a b X H0 H1 => proj1 (Zsub_pos_bound_div a b X H0 H1))