no goals
R : Type u_2
S : Type u_1
inst✝¹ : Ring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
a b c : R
⊢ ↑abv (a - c) ≤ ↑abv (a - b) + ↑abv (b - c)
simpa [sub_eq_add_neg, add_assoc] using abv.add_le (a - b) (b - c)