From 636ba579315b8f1fadf3714097d61378e3eff528 Mon Sep 17 00:00:00 2001
From: Jade Philipoom <jadep@google.com>
Date: Fri, 16 Feb 2018 18:15:18 +0100
Subject: add three proofs to ZUtil

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

(limited to 'src/Util/ZUtil')

diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v
index d402055dd..e0a80544d 100644
--- a/src/Util/ZUtil/Modulo.v
+++ b/src/Util/ZUtil/Modulo.v
@@ -222,6 +222,9 @@ Module Z.
     : 0 <= c -> (a / b) mod c = a mod (c * b) / b.
   Proof. rewrite mod_pull_div_full; destruct (c <? 0) eqn:?; Z.ltb_to_lt; simpl; omega. Qed.
 
+  Lemma small_mod_eq a b n: a mod n = b mod n -> 0 <= a < n -> a = b mod n.
+  Proof. intros; rewrite <-(Z.mod_small a n); auto. Qed.
+
   Lemma mod_pow_full p q n : (p^q) mod n = ((p mod n)^q) mod n.
   Proof.
     destruct (Z_dec' n 0) as [ [H|H] | H]; subst;
-- 
cgit v1.2.3