diff options
Diffstat (limited to 'src/ModularArithmetic/Montgomery/ZBounded.v')
-rw-r--r-- | src/ModularArithmetic/Montgomery/ZBounded.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Montgomery/ZBounded.v b/src/ModularArithmetic/Montgomery/ZBounded.v index d01a48d89..2da20ddcf 100644 --- a/src/ModularArithmetic/Montgomery/ZBounded.v +++ b/src/ModularArithmetic/Montgomery/ZBounded.v @@ -78,7 +78,7 @@ Section montgomery. eauto 6 using reduce_via_partial_correct, reduce_via_partial_in_range, decode_small_valid. Qed. - Theorem reduce_via_partial_correct + Lemma reduce_via_partial_correct'' : Z.equiv_modulo modulus (decode_small (proj1_sig (reduce_via_partial v))) (decode_large v * R') @@ -88,5 +88,13 @@ Section montgomery. apply decode_small_valid in H'. destruct reduce_via_partial_correct'; split; eauto; omega. Qed. + + Theorem reduce_via_partial_correct + : decode_small (proj1_sig (reduce_via_partial v)) = (decode_large v * R') mod modulus. + Proof. + rewrite <- (proj1 reduce_via_partial_correct''). + rewrite Z.mod_small by apply reduce_via_partial_correct''. + reflexivity. + Qed. End correctness. End montgomery. |