R : Type u_2
S : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ ↑abv b - ↑abv a ≤ ↑abv (b - a)
R : Type u_2
S : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ ↑abv b - ↑abv a ≤ ↑abv (a - b)
rw [abv.map_sub]
no goals
R : Type u_2
S : Type u_1
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
a b : R
⊢ ↑abv b - ↑abv a ≤ ↑abv (b - a)
apply abv.le_sub