From 27af16da0a0d4ace1b3b691df61da7b1db807e99 Mon Sep 17 00:00:00 2001
From: Jade Philipoom <jadep@mit.edu>
Date: Mon, 15 Feb 2016 18:48:56 -0500
Subject: a few lemmas in util about powers of 2 in Bedrock's various rewritten
 forms

---
 src/Util/NatUtil.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/Util/NatUtil.v')

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.
-- 
cgit v1.2.3