From f4e35faa34145ab24aad021025b7d0d6e7f2214c Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Thu, 21 Jul 2016 13:49:52 -0700
Subject: Add more ZUtil

---
 src/Util/ZUtil.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'src')

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 370628b3c..d0aa12e58 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -984,6 +984,22 @@ Module Z.
   Qed.
 
   Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using lia : zsimplify.
+
+  Lemma div_small_neg x y : 0 < -x < y -> x / y = -1.
+  Proof.
+    intro H; rewrite <- (Z.opp_involutive x).
+    rewrite Z.div_opp_l_complete by lia.
+    generalize dependent (-x); clear x; intros x H.
+    autorewrite with zsimplify; break_match; lia.
+  Qed.
+  Hint Rewrite div_small_neg using lia : zsimplify.
+
+  Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y < z -> (x - y) / z = if x <? y then -1 else 0.
+  Proof.
+    pose proof (Zlt_cases x y).
+    intros; break_match; autorewrite with zsimplify; lia.
+  Qed.
+  Hint Rewrite div_small_neg using lia : zsimplify.
 End Z.
 
 Module Export BoundsTactics.
-- 
cgit v1.2.3