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