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.
