diff options
| author |  David Benjamin <davidben@google.com> | 2018-02-24 18:20:12 -0500 |
|---|---|---|
| committer |  Andres Erbsen <andreser@mit.edu> | 2018-03-09 18:02:01 -0500 |
| commit | 0a556929568e0fc3255cc160fa4b35a75eb14f60 (patch) | |
| tree | 0654f54711c6ca1d0ff0c5d2e2e319f3915a5c8f /coqprime | |
| parent | 22f92f15e8b42cdb9db06a421986a36f4a76d05a (diff) | |
Review comments.
Major change is porting everything to Z and using Z.div_mod_to_quot_rem
which is a handy sledgehammer. Z is also a nice simplification. Dealing
with subtraction is tidier, though I do have 0 <= x goals everywhere as
a result.
Diffstat (limited to 'coqprime')
0 files changed, 0 insertions, 0 deletions