no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c : α
⊢ abs (max a c - max b c) ≤ abs (a - b)
simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg (a - b))]
  using abs_max_sub_max_le_max a c b c