1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index afed2a231..256654df7 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,4 +1,7 @@
 Require Import NPeano Omega.
+Require Import Bedrock.Word.
+
+Local Open Scope nat_scope.
 
 Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1.
 Proof.
@@ -54,3 +57,8 @@ Proof.
     rewrite <- nat_compare_lt; auto.
   }
 Qed.
+
+Lemma pow2_id : forall n, pow2 n = 2 ^ n.
+Proof.
+  induction n; intros; simpl; auto.
+Qed.