a b c : Int
h✝ : a + b < c
h : -a + (a + b) < -a + c
⊢ b < -a + c
a b c : Int
h : a + b < c
⊢ b < -a + c
have h := Int.add_lt_add_left h (-a)
no goals
a b c : Int
h✝ : a + b < c
h : -a + (a + b) < -a + c
⊢ b < -a + c
rwa [Int.neg_add_cancel_left] at h