Theorem: abs_sub_le' (GlimpseOfLean/Library/Basic.lean)

State before:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a - c| ≤ |a - b| + |c - b|
Tactic:
rw [abs_sub_comm c b]
State after:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a - c| ≤ |a - b| + |b - c|

State before:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a - c| ≤ |a - b| + |b - c|
Tactic:
apply abs_sub_le
State after:
no goals