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.lt_neg_add_of_add_lt (Int.sub_left_lt_of_lt_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