diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-01-05 18:22:29 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-01-05 18:22:29 -0500 |
| commit | b054c75690ab33b71d4a6abf57715c573f924aec (patch) | |
| tree | c52395852f4e724f0fe45aa2dd48f7d49f898495 /src/Util/ZUtil.v | |
| parent | e513f01db4f7bbf0e51aadd7e1a9530201d427b6 (diff) | |
Util: added util lemmas needed to instantiate EdDSA25519.
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 5950f57ad..1a48abfd6 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,5 +1,7 @@ Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv. Require Import Omega NPeano Arith. +Require Import Crypto.Util.NatUtil. +Require Import Bedrock.Word. Local Open Scope Z. Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. @@ -50,3 +52,15 @@ Qed. Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0. intuition. Qed. + +Lemma Zpow_pow2 : forall n, (pow2 n)%nat = Z.to_nat (2 ^ (Z.of_nat n)). +Proof. + induction n; intros; auto. + simpl pow2. + rewrite Nat2Z.inj_succ. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite untimes2. + rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega). + rewrite <- IHn. + auto. +Qed. |