diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-15 18:48:56 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-02-15 18:48:56 -0500 |
| commit | 27af16da0a0d4ace1b3b691df61da7b1db807e99 (patch) | |
| tree | 708a2a9bf66ab46ff143bfc912661223c70e2a10 /src/Util/NatUtil.v | |
| parent | ff2eb39f8c33b83d3c6a8ddf029bbff96626e429 (diff) | |
a few lemmas in util about powers of 2 in Bedrock's various rewritten forms
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 8 |
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. |