diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-11 22:39:00 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-11 22:39:00 -0400 |
| commit | ef4a656933ce31144ad11f83b7f6a0758cd7e518 (patch) | |
| tree | cf412e453462843e4d02b5bf342bd50cb1620219 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | ce1a0e8508f53481138362f14581193b7394552b (diff) | |
Merge and refactor of GF25519
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 7efccbade..0a7070922 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -94,7 +94,9 @@ Section PseudoMersenneProofs. replace (2^k) with ((2^k - c) + c) by ring. rewrite Z.mul_add_distr_r. rewrite Zplus_mod. - rewrite <- modulus_pseudomersenne. + unfold c. + rewrite Z.sub_sub_distr, Z.sub_diag. + simpl. rewrite Z.mul_comm. rewrite mod_mult_plus; auto using modulus_nonzero. rewrite <- Zplus_mod; auto. @@ -379,7 +381,7 @@ Section CarryProofs. rewrite Z.mul_comm. rewrite Z.mul_assoc. rewrite <- Z.pow_add_r by (apply log_cap_nonneg || apply sum_firstn_limb_widths_nonneg). - rewrite <- k_matches_limb_widths. + unfold k. replace (length limb_widths) with (S (pred (length base))) by (subst; rewrite <- base_length; apply NPeano.Nat.succ_pred; omega). rewrite sum_firstn_succ with (x:= log_cap (pred (length base))) by |