no goals
a b : Int
H : NonNeg (-(b - a))
⊢ b ≤ a
rwa [show -(b - a) = a - b by simp [Int.add_comm, Int.sub_eq_add_neg]] at H
no goals
a b : Int
H : NonNeg (-(b - a))
⊢ -(b - a) = a - b
simp [Int.add_comm, Int.sub_eq_add_neg]