From a0fab645d1fd01e56c7d6b78178d77eaddbd02e6 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 3 Nov 2017 00:47:54 -0400
Subject: Add value_modulo_in_range

---
 src/Util/ZBounded.v | 9 +++++++++
 1 file changed, 9 insertions(+)

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

diff --git a/src/Util/ZBounded.v b/src/Util/ZBounded.v
index 64cb57b0a..4e0309053 100644
--- a/src/Util/ZBounded.v
+++ b/src/Util/ZBounded.v
@@ -152,3 +152,12 @@ Proof.
   rewrite Z.mod_small by omega.
   omega.
 Qed.
+
+Lemma value_modulo_in_range z r (Hr : lower r <= z <= upper r)
+  : value (modulo z r) = z.
+Proof.
+  simpl.
+  destruct (upper r <? lower r) eqn:H'; [ reflexivity | ].
+  rewrite Z.mod_small by omega.
+  omega.
+Qed.
-- 
cgit v1.2.3