rw [max_comm]
case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|
case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |b| |a|