no goals
S : Type u_1
inst✝² : OrderedRing S
R : Type u_2
inst✝¹ : Ring R
abv : R → S
inst✝ : IsAbsoluteValue abv
a b c : R
⊢ abv (a - c) ≤ abv (a - b) + abv (b - c)
simpa [sub_eq_add_neg, add_assoc] using abv_add abv (a - b) (b - c)