a b c : Int
h : a + b < a + c
this : -a + (a + b) < -a + (a + c)
⊢ b < c
a b c : Int
h : a + b < a + c
⊢ b < c
have : -a + (a + b) < -a + (a + c) := Int.add_lt_add_left h _
a b c : Int
h : a + b < a + c
this : b < c
⊢ b < c
a b c : Int
h : a + b < a + c
this : -a + (a + b) < -a + (a + c)
⊢ b < c
simp [Int.neg_add_cancel_left] at this
no goals
a b c : Int
h : a + b < a + c
this : b < c
⊢ b < c
assumption