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

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