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