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