rw [← add_zero a, ← sub_add_cancel b a, add_comm (b - a)]
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : 0 ≤ b - a
⊢ a ≤ b
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : 0 ≤ b - a
⊢ a + 0 ≤ a + (b - a)