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