mathlib
7dc33bf7 - feat(data/nat/basic): Some `nat.find` lemmas (#10263)

Commit
4 years ago
feat(data/nat/basic): Some `nat.find` lemmas (#10263) This proves `nat.find_le` and `nat.find_add` and renames the current `nat.find_le` to `nat.find_mono`.
Author
Parents
Loading