diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-18 21:19:00 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-18 21:19:00 -0400 |
| commit | 6cf84dda56b7d518349f4c138192a4fe164f8e65 (patch) | |
| tree | d4d49124eac7f1ef5f96a405dab6a56baaabed4b /src/Util/ZUtil | |
| parent | 4ca9c661db6d99a98075c566cc74c9352b2a9c8c (diff) | |
Add Z.div_nonneg
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/Div.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index 31237d679..9cbda2d85 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -109,4 +109,10 @@ Module Z. Lemma div_le_mono_pow_pos a b c e : a <= b -> a / Z.pos c ^ e <= b / Z.pos c ^ e. Proof. auto with zarith. Qed. + + Lemma div_nonneg a b : 0 <= a -> 0 <= b -> 0 <= a / b. + Proof. + destruct (Z_zerop b); subst; rewrite ?Zdiv_0_r; [ reflexivity | ]. + intros; apply Z.div_pos; omega. + Qed. End Z. |