diff options
| author |  David Benjamin <davidben@google.com> | 2018-01-15 02:47:15 -0500 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2018-01-15 04:12:08 -0500 |
| commit | 36e2e828be55cb58f985208de0ef7085cedecdd2 (patch) | |
| tree | 940c03e8a9988e07e0272f689a88d3f2c243ae9c /_CoqProject | |
| parent | e30d9e19b4b12ea9388b13d7c1ab2ffc5aba4917 (diff) | |
Combine the zero and non-zero cases together.
This required tending to montladder not being proved Feq-preserving
(sidestepped by proving for all P = 0), and then some wrestling with
scalarmult to show the right-hand side was indeed zero when x is (0, 0).
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions