with_bot): `n < m → n + 1 ≤ m` (#18174)

Commit

2 years ago

feat(data/nat/with_bot): `n < m → n + 1 ≤ m` (#18174) ported in https://github.com/leanprover-community/mathlib4/pull/1519

Author

alreadydone

Parents