add three proofs to ZUtil

2 files changed, 15 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 973c2685d..2ff1ef834 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -964,6 +964,18 @@ Module Z.
   Qed.
   Hint Resolve div_sub_mod_cond : zarith.
 
+  Lemma div_add_mod_cond_l : forall x y d, d <> 0 -> (x + y) / d = (x mod d + y) / d + x / d.
+  Proof.
+    intros. replace (x + y) with ((x - x mod d) + (x mod d + y)) by lia.
+    rewrite Z.div_add_exact by auto with zarith.
+    rewrite <- Z.div_sub_mod_exact by lia; lia.
+  Qed.
+
+  Lemma div_add_mod_cond_r : forall x y d, d <> 0 -> (x + y) / d = (x + y mod d) / d + y / d.
+  Proof.
+    intros. rewrite Z.add_comm, div_add_mod_cond_l by auto. repeat (f_equal; try ring).
+  Qed.
+
   Lemma div_between n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a / b = n.
   Proof. intros; Z.div_mod_to_quot_rem; nia. Qed.
   Hint Rewrite div_between using zutil_arith : zsimplify.
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;