diff options
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 4 |
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. |