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 /coqprime/Coqprime | |
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 'coqprime/Coqprime')
0 files changed, 0 insertions, 0 deletions