Move two_k_nonzero to PseudoMersenneBaseParamProofs.v

It has nothing to do with ext_base

2 files changed, 7 insertions, 7 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).
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index e0a194c3b..07114b1e4 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -25,6 +25,12 @@ Section PseudoMersenneBaseParamProofs.
     apply sum_firstn_limb_widths_nonneg; auto.
   Qed. Hint Resolve k_nonneg.
 
+  Lemma two_k_nonzero : 2^k <> 0.
+  Proof.
+    pose proof (Z.pow_eq_0 2 k k_nonneg).
+    intuition.
+  Qed.
+
   Lemma base_matches_modulus: forall i j,
     (i   <  length limb_widths)%nat ->
     (j   <  length limb_widths)%nat ->
@@ -81,4 +87,4 @@ Section PseudoMersenneBaseParamProofs.
     base_good := base_good
   }.
 
-End PseudoMersenneBaseParamProofs.
\ No newline at end of file
+End PseudoMersenneBaseParamProofs.