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