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