From bd342ca00d6251e509bd9f9cff2a5bf92e6d51b9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Jul 2016 10:33:24 -0700 Subject: Add pow2_mod to ZUtil --- src/Util/ZUtil.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/Util/ZUtil.v') 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. -- cgit v1.2.3