Strict additive monotonicity on WithBot ℕ

Mathlib's WithBot.add_lt_add_of_le_of_lt / WithBot.add_lt_add_of_lt_of_le carry ≠ ⊥ side conditions; the fully strict version below needs none of them over ℕ. Upstreaming candidate.

theorem WithBot.add_lt_add {a b c d : WithBot ℕ} (h1 : a < b) (h2 : c < d) : a + c < b + d

Strict monotonicity of + on WithBot ℕ: a < b → c < d → a + c < b + d.