diff options
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel2.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index 6cd771e57..e35e14616 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -2924,7 +2924,8 @@ Module Montgomery256. xy = true -> expr.Interp (@ident.interp) montred256 xy = MontgomeryReduction.montred' N R N' (Z.log2 R) 2 2 xy. Proof. intros; rewrite montred256_correct_proj2 by assumption; unfold app_curried; exact eq_refl. Qed. -*) + *) + Local Arguments is_bounded_by_bool / . Lemma montred256_correct_full R' (R'_correct : Z.equiv_modulo N (R * R') 1) : forall (lo hi : Z), 0 <= lo < R -> 0 <= hi < R -> 0 <= lo + R * hi < R * N -> |