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/PseudoMersenneBaseParamProofs.v | |
| parent | 70f3ef2ad457248aeb361c68af25a74169e0e861 (diff) | |
Move two_k_nonzero to PseudoMersenneBaseParamProofs.v
It has nothing to do with ext_base
Diffstat (limited to 'src/ModularArithmetic/PseudoMersenneBaseParamProofs.v')
| -rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 8 |
1 files changed, 7 insertions, 1 deletions
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. |