Theorem: aux1 (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 : a ≤ b
⊢ 0 ≤ b - a
Tactic:
rw [← sub_self a, sub_eq_add_neg, sub_eq_add_neg, add_comm, add_comm b]
State after:
R : Type u_1
inst✝ : StrictOrderedRing R
a b c : R
h : a ≤ b
⊢ -a + a ≤ -a + b

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