[GOAL]
a b : ℕ
h : 0 < b
⊢ a + 0 < a + b
[PROOFSTEP]
apply Nat.add_lt_add_left
[GOAL]
case h
a b : ℕ
h : 0 < b
⊢ 0 < b
[PROOFSTEP]
assumption
[GOAL]
a : ℕ
this : 0 < a + 1
⊢ 0 < 1 + a
[PROOFSTEP]
simp [Nat.add_comm]
[GOAL]
a : ℕ
this : 0 < a + 1
⊢ 0 < a + 1
[PROOFSTEP]
assumption
