Commit 2019-11-09 19:14 1236ced4
View on Github →feat(data/nat/basic): succ_div (#1664)
- feat(data/nat/basic): succ_div Rather long proof, but it was the best I could do.
- Update basic.lean
- add the two lemmas for each case
- get rid of positivity assumption