a b : Int
h : a < b
this : 0 < -a + b
⊢ -b < -a
a b : Int
h : a < b
⊢ -b < -a
have : 0 < -a + b := Int.add_left_neg a ▸ Int.add_lt_add_left h (-a)
a b : Int
h : a < b
this✝ : 0 < -a + b
this : 0 + -b < -a + b + -b
⊢ -b < -a
a b : Int
h : a < b
this : 0 < -a + b
⊢ -b < -a
have : 0 + -b < -a + b + -b := Int.add_lt_add_right this (-b)
no goals
a b : Int
h : a < b
this✝ : 0 < -a + b
this : 0 + -b < -a + b + -b
⊢ -b < -a
rwa [Int.add_neg_cancel_right, Int.zero_add] at this