diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-07 10:33:24 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-07 10:33:24 -0700 |
| commit | bd342ca00d6251e509bd9f9cff2a5bf92e6d51b9 (patch) | |
| tree | 3ab4dfa60fceabac0578c023c1cda952474f9f8c /src/Util/ZUtil.v | |
| parent | b2b83c0f7e903abf8755a85694c7acd9aa139107 (diff) | |
Add pow2_mod to ZUtil
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 263d94fa2..219165d08 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -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. |