a b c : Int
h✝ : b < c - a
h : a + b < a + (c - a)
⊢ a + b < c
a b c : Int
h : b < c - a
⊢ a + b < c
have h := Int.add_lt_add_left h a
no goals
a b c : Int
h✝ : b < c - a
h : a + b < a + (c - a)
⊢ a + b < c
rwa [← Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h