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