Theorem: aux2 (LeanInRome/S2_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean)

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

State before:
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : 0 ≤ b - a
⊢ a + 0 ≤ a + (b - a)
Tactic:
apply add_le_add_left h
State after:
no goals