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