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