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