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