merge

1 files changed, 3 insertions, 1 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 845a2e9c0..2bcbabaac 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -22,7 +22,7 @@ Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z
     this database. *)
 Create HintDb zsimplify discriminated.
 Hint Rewrite Z.div_1_r Z.mul_1_r Z.mul_1_l Z.sub_diag Z.mul_0_r Z.mul_0_l Z.add_0_l Z.add_0_r Z.opp_involutive Z.sub_0_r : zsimplify.
-Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add using lia : zsimplify.
+Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z.div_add Z.div_add_l Z.mod_add Z.div_0_l using lia : zsimplify.
 
 (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *)
 Create HintDb push_Zopp discriminated.
@@ -49,6 +49,8 @@ Hint Rewrite Z.div_small_iff using lia : zstrip_div.
 Create HintDb zstrip_div.
 
 Module Z.
+  Definition pow2_mod n i := (n & (Z.ones i)).
+
   Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
   Proof. intros; omega. Qed.