a b c : Int
h✝ : a + b ≤ c
h : a + b + -b ≤ c + -b
⊢ a ≤ c - b
a b c : Int
h : a + b ≤ c
⊢ a ≤ c - b
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 ≤ c - b
rwa [Int.add_neg_cancel_right] at h