no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b✝ c✝ a b c d : α
⊢ abs (min a b - min c d) ≤ max (abs (a - c)) (abs (b - d))
simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm] using
  abs_max_sub_max_le_max (-a) (-b) (-c) (-d)