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