diff options
author | Jason Gross <jagro@google.com> | 2018-08-13 18:46:52 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-08-13 18:46:52 -0400 |
commit | c22b3c9726aa1c052fd44bcaf0ced8fb30970206 (patch) | |
tree | 4937a0d4d71ba5d3bdffb4dd16341a83917f6182 /src/Util/ZUtil/Div.v | |
parent | cd24907d7c46ddc52989a5cfa7a10c3c4568eee3 (diff) |
Fix split_bounds, prove it correct
Diffstat (limited to 'src/Util/ZUtil/Div.v')
-rw-r--r-- | src/Util/ZUtil/Div.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index a9fc4aae0..5ae17ad1a 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -258,4 +258,8 @@ Module Z. intros; subst; auto with zarith. Qed. Hint Resolve div_same' : zarith. + + Lemma div_opp_r a b : a / (-b) = ((-a) / b). + Proof. Z.div_mod_to_quot_rem; nia. Qed. + Hint Resolve div_opp_r : zarith. End Z. |