rw [← sub_self a, sub_eq_add_neg, sub_eq_add_neg, add_comm, add_comm b]
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : a ≤ b
⊢ 0 ≤ b - a
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : a ≤ b
⊢ -a + a ≤ -a + b