diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-20 17:08:09 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-20 17:08:09 -0400 |
| commit | cb7580b8f501bfadd8792ea3b8d50f89df5a656a (patch) | |
| tree | 6a832aaa85445fae28c63083492ff659caaed9e9 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | 55e6291f60ff65fa484a7bad1806adcf4be78cf1 (diff) | |
| parent | 476f078855a221a2ec47a63e7efdceaa35acd488 (diff) | |
Merge branch 'master' of github.com:mit-plv/fiat-crypto
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 76a7399e3..e6351dc17 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -106,14 +106,6 @@ Section PseudoMersenneProofs. Local Hint Resolve firstn_us_base_ext_base bv ExtBaseVector limb_widths_match_modulus. Local Hint Extern 1 => apply limb_widths_match_modulus. - Lemma mul_rep_extended : forall (us vs : BaseSystem.digits), - (length us <= length base)%nat -> - (length vs <= length base)%nat -> - (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode (ext_base limb_widths) (BaseSystem.mul (ext_base limb_widths) us vs). - Proof. - intros; apply mul_rep_two_base; auto with arith distr_length. - Qed. - Lemma modulus_nonzero : modulus <> 0. pose proof (Znumtheory.prime_ge_2 _ prime_modulus); omega. Qed. |