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