α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ abs (a + -b) ≤ abs a + abs (-b)
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ abs (a - b) ≤ abs a + abs b
rw [sub_eq_add_neg, ← abs_neg b]
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c d a b : α
⊢ abs (a + -b) ≤ abs a + abs (-b)
exact abs_add a _