diff options
author | Jason Gross <jagro@google.com> | 2016-07-19 14:55:56 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-19 14:55:56 -0700 |
commit | af5bff992249f84cbb0c0dc38c273b974bf07a41 (patch) | |
tree | eb283c3940a3c8aaec9370587e0e80897622b613 /src/ModularArithmetic/ExtendedBaseVector.v | |
parent | 70f3ef2ad457248aeb361c68af25a74169e0e861 (diff) |
Move two_k_nonzero to PseudoMersenneBaseParamProofs.v
It has nothing to do with ext_base
Diffstat (limited to 'src/ModularArithmetic/ExtendedBaseVector.v')
-rw-r--r-- | src/ModularArithmetic/ExtendedBaseVector.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index 0afd6b484..e2fcab9a0 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -83,12 +83,6 @@ Section ExtendedBaseVector. destruct (lt_dec 0 (length base)); try apply BaseSystem.b0_1; try omega. Qed. - Lemma two_k_nonzero : 2^k <> 0. - Proof. - pose proof (Z.pow_eq_0 2 k k_nonneg). - intuition. - Qed. - Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> nth_default 0 (map (Z.mul (2 ^ k)) base) n = (2 ^ k) * (nth_default 0 base n). |