aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Util/ZUtil/Div.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v
index 9cbda2d85..9b63fadae 100644
--- a/src/Util/ZUtil/Div.v
+++ b/src/Util/ZUtil/Div.v
@@ -115,4 +115,5 @@ Module Z.
destruct (Z_zerop b); subst; rewrite ?Zdiv_0_r; [ reflexivity | ].
intros; apply Z.div_pos; omega.
Qed.
+ Hint Resolve div_nonneg : zarith.
End Z.