1 files changed, 26 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Pow2.v b/src/Util/ZUtil/Pow2.v
new file mode 100644
index 000000000..bc3b01225
--- /dev/null
+++ b/src/Util/ZUtil/Pow2.v
@@ -0,0 +1,26 @@
+Require Import Coq.micromega.Lia.
+Require Import Coq.ZArith.ZArith.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma pow2_ge_0: forall a, (0 <= 2 ^ a)%Z.
+  Proof.
+    intros; apply Z.pow_nonneg; omega.
+  Qed.
+
+  Lemma pow2_gt_0: forall a, (0 <= a)%Z -> (0 < 2 ^ a)%Z.
+  Proof.
+    intros; apply Z.pow_pos_nonneg; [|assumption]; omega.
+  Qed.
+
+  Lemma pow2_lt_or_divides : forall a b, 0 <= b ->
+    2 ^ a < 2 ^ b \/ (2 ^ a) mod 2 ^ b = 0.
+  Proof.
+    intros a b H.
+    destruct (Z_lt_dec a b); [left|right].
+    { apply Z.pow_lt_mono_r; auto; omega. }
+    { replace a with (a - b + b) by ring.
+      rewrite Z.pow_add_r by omega.
+      apply Z.mod_mul, Z.pow_nonzero; omega. }
+  Qed.
+End Z.