diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-10 00:43:01 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-10 12:14:23 -0400 |
| commit | 1ff16cf798e249cd6b8e9a0d47f0db19b510c807 (patch) | |
| tree | 751c8d9444dee59668fe8603b8abaae1496dd28d /src/Arithmetic/MontgomeryReduction | |
| parent | 4b31576821213bccba9513918d44f34883cf8bde (diff) | |
Add redc_bound
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index e0b2d26d6..7c5c51bf0 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -312,4 +312,12 @@ Section WordByWordMontgomery. autorewrite with push_eval zsimplify; [ | rewrite Npos_correct; pose proof (eval_nonneg B); lia ]. Admitted. + + Lemma redc_bound A + : 0 <= eval (redc A) < eval N + eval B. + Proof. + unfold redc. + apply redc_loop_bound; simpl; autorewrite with push_eval. + rewrite Npos_correct; pose proof (eval_nonneg B); lia. + Qed. End WordByWordMontgomery. |