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