From 78656baa06ed1daeb7ba90c2d429228516dc8475 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Tue, 26 Jun 2018 15:10:24 -0400
Subject: Add a couple of zrange lemmas

---
 src/Util/ZRange.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/Util/ZRange.v')

diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v
index 4f1e4f806..8badcb492 100644
--- a/src/Util/ZRange.v
+++ b/src/Util/ZRange.v
@@ -68,6 +68,9 @@ Proof.
   split; intro H; (repeat let x := fresh in intro x; specialize (H x)); omega.
 Qed.
 
+Definition is_bounded_by_bool (v : Z) (x : zrange) : bool
+  := ((lower x <=? v) && (v <=? upper x))%bool%Z.
+
 Definition is_tighter_than_bool (x y : zrange) : bool
   := ((lower y <=? lower x) && (upper x <=? upper y))%bool%Z.
 
-- 
cgit v1.2.3