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_le_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