α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ abs b - abs a ≤ abs (b - a)
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ abs b - abs a ≤ abs (a - b)
rw [abs_sub_comm]
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ abs b - abs a ≤ abs (b - a)
apply abs_sub_abs_le_abs_sub