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