From af5bff992249f84cbb0c0dc38c273b974bf07a41 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 14:55:56 -0700 Subject: Move two_k_nonzero to PseudoMersenneBaseParamProofs.v It has nothing to do with ext_base --- src/ModularArithmetic/ExtendedBaseVector.v | 6 ------ src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 8 +++++++- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3