a b : Int
h✝ : 0 ≤ a - b
h : 0 + b ≤ a - b + b
⊢ b ≤ a
a b : Int
h : 0 ≤ a - b
⊢ b ≤ a
have h := Int.add_le_add_right h b
no goals
a b : Int
h✝ : 0 ≤ a - b
h : 0 + b ≤ a - b + b
⊢ b ≤ a
rwa [Int.sub_add_cancel, Int.zero_add] at h