aboutsummaryrefslogtreecommitdiff
path: root/src/Util/ZUtil/Div.v
Commit message (Expand)AuthorAge
* add some hints to the global databasesGravatar jadep2019-03-26
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Fix split_bounds, prove it correctGravatar Jason Gross2018-08-13
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Shuffle some ZUtil lemmas aroundGravatar Jason Gross2018-07-08
* add some lemmas aboud div and modGravatar Jade Philipoom2018-04-11
* prove stronger bound on quotient error for barrett reductionGravatar Jade Philipoom2018-04-11
* move some lemmas to ZUtil/ListUtilGravatar Jade Philipoom2018-04-03
* move things from ZUtil.v into Div.vGravatar Jade Philipoom2018-02-23
* Add div_nonneg to zarithGravatar Jason Gross2017-06-18
* Add Z.div_nonnegGravatar Jason Gross2017-06-18
* Add Z.div_le_mono_nonnegGravatar Jason Gross2017-05-13
* Split off more ZUtil thingsGravatar Jason Gross2017-05-13
* Split off more of ZUtilGravatar Jason Gross2017-05-13