diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2015-11-07 13:25:34 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2015-11-07 13:27:36 -0500 |
| commit | b953c040b36f34b480759f0c4cd275eff4d1efa5 (patch) | |
| tree | dd2f6e1b0ac2613ce1f532376daee0ab11a87f54 /src/Specific/GF25519.v | |
| parent | 9e767c9bfe4158215e4efaa1a4cc1744bb0b2b58 (diff) | |
ModularBaseSystem: prove some admits in mase system extension
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index c0e330825..4925f87c5 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -55,8 +55,8 @@ Module GF25519Base25Point5Params <: PseudoMersenneBaseParams Base25Point5_10limb (j < length base)%nat -> (i+j >= length base)%nat -> let b := nth_default 0 base in - let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in - b i * b j = r * 2^k * b (i+j-length base)%nat. + let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in + b i * b j = r * (2^k * b (i+j-length base)%nat). Proof. intros. assert (In i (seq 0 (length base))) by nth_tac. |