Add a variant of add_shift_mod

1 files changed, 9 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 4f3596737..3a640e866 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1829,6 +1829,15 @@ Module Z.
     apply Z.div_small; split; nia.
   Qed.
 
+  Lemma add_mul_mod x y n m
+        (Hx : 0 <= x < 2^n) (Hy : 0 <= y < m)
+        (Hn : 0 <= n)
+    : (x + y * 2^n) mod (m * 2^n) = x + (y mod m) * 2^n.
+  Proof.
+    generalize (add_shift_mod x y n m).
+    autorewrite with Zshift_to_pow; auto.
+  Qed.
+
   Lemma lt_pow_2_shiftr : forall a n, 0 <= a < 2 ^ n -> a >> n = 0.
   Proof.
     intros.