theorem Nat.lt_add_of_zero_lt_left (a : ℕ) (b : ℕ) (h : 0 < b) : a < a + b

theorem Nat.zero_lt_one_add (a : ℕ) : 0 < 1 + a

theorem Nat.lt_add_left (a : ℕ) (b : ℕ) (c : ℕ) : a < b → a < c + b