a b : Int
h : 0 < b
this : a + 0 < a + b
⊢ a < a + b
a b : Int
h : 0 < b
⊢ a < a + b
have : a + 0 < a + b := Int.add_lt_add_left h a
no goals
a b : Int
h : 0 < b
this : a + 0 < a + b
⊢ a < a + b
rwa [Int.add_zero] at this