diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-18 21:19:50 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-18 21:19:50 -0400 |
| commit | 6f9a2b0e28c9511712489929c88c4e9717aee8de (patch) | |
| tree | 9eaea9fe8f59ed1c208b88151d8c00b27f1d581e /src/Util/ZUtil | |
| parent | 6cf84dda56b7d518349f4c138192a4fe164f8e65 (diff) | |
Add div_nonneg to zarith
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/Div.v | 1 |
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. |