diff options
| -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 5c13c319d..d06477d3c 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -298,7 +298,7 @@ Module Z. Lemma div_lt_upper_bound' a b q : 0 < b -> a < q * b -> a / b < q. Proof. intros; apply Z.div_lt_upper_bound; nia. Qed. - Hint Resolve Z.div_lt_upper_bound : zarith. + Hint Resolve div_lt_upper_bound' : zarith. Lemma mul_comm3 x y z : x * (y * z) = y * (x * z). Proof. lia. Qed. |