diff options
| -rw-r--r-- | src/Arithmetic/Saturated/MontgomeryAPI.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v index de1f4a754..7e755e64d 100644 --- a/src/Arithmetic/Saturated/MontgomeryAPI.v +++ b/src/Arithmetic/Saturated/MontgomeryAPI.v @@ -358,7 +358,8 @@ Section API. subst x. rewrite @B.Positional.sat_add_div by omega. repeat match goal with H:_|-_=> unique pose proof (eval_small _ _ H) end. - Admitted. + cbv [eval] in *; Z.div_mod_to_quot_rem; nia. + Qed. Lemma small_add_S1 n a b : (2 <= bound) -> |