a b c : Int
h✝ : b ≤ c - a
h : a + b ≤ a + (c - a)
⊢ a + b ≤ c
a b c : Int
h : b ≤ c - a
⊢ a + b ≤ c
have h := Int.add_le_add_left h a
no goals
a b c : Int
h✝ : b ≤ c - a
h : a + b ≤ a + (c - a)
⊢ a + b ≤ c
rwa [← Int.add_sub_assoc, Int.add_comm a c, Int.add_sub_cancel] at h