diff options
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
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)) |