Commit 2020-10-06 22:45 f4ccbdf5

feat(data/nat/basic): add_succ_lt_add (#4483) Add the lemma that, for natural numbers, if a < b and c < d then a + c + 1 < b + d (i.e. a stronger version of add_lt_add for the natural number case). library_search did not find this in mathlib.