a b c : Int
h✝ : -b + a ≤ c
h : b + (-b + a) ≤ b + c
⊢ a ≤ b + c
a b c : Int
h : -b + a ≤ c
⊢ a ≤ b + c
have h := Int.add_le_add_left h b
no goals
a b c : Int
h✝ : -b + a ≤ c
h : b + (-b + a) ≤ b + c
⊢ a ≤ b + c
rwa [Int.add_neg_cancel_left] at h