As an experiment, I tried to prove this using $ (0) \;\;\; |p| = p \max -p $ together with the properties of $\;\max\;$ (and $\;\min\;$). The result is not too pretty, but the upside is that I could do it almost mechanically, and without any case distinctions.
Let's first start with the following subexpression: \begin{align} & |x| - |y| \\ = & \;\;\;\;\;\text{"definition $(0)$, twice"} \\ & (x \max -x) - (y \max -y) \\ = & \;\;\;\;\;\text{"$\;-\;$ distributes over $\;\max\;$ to the left"} \\ & (x - (y \max -y)) \;\max\; (-x - (y \max -y)) \\ = & \;\;\;\;\;\text{"a DeMorgan-like rule"} \\ & (x + (-y \min y)) \;\max\; (-x + (-y \min y)) \\ = & \;\;\;\;\;\text{"$\;+\;$ distributes over $\;\min\;$"} \\ & ((x - y) \min (x + y)) \;\max\; ((-x - y) \min (-x + y)) \\ \end{align} so we've proven $ (1) \;\;\; |x| - |y| \;=\; ((x - y) \min (x + y)) \;\max\; ((-x - y) \min (-x + y)) $ Now we use this to rewrite the left hand side of our original equation: \begin{align} & \big||x| - |y|\big| \\ = & \;\;\;\;\;\text{"definition $(0)$"} \\ & (|x| - |y|) \;\max\; (|y| - |x|) \\ = & \;\;\;\;\;\text{"property $(1)$, twice"} \\ & ((x - y) \min (x + y)) \;\max\; ((-x - y) \min (-x + y)) \;\max\; \\ & ((y - x) \min (y + x)) \;\max\; ((-y - x) \min (-y + x)) \\ = & \;\;\;\;\;\text{"exchange the second and third terms; rewrite some sums"} \\ & ((x - y) \min (x + y)) \;\max\; ((y - x) \min (x + y)) \;\max\; \\ & ((-x - y) \min (y - x)) \;\max\; ((-x - y) \min (x - y)) \\ = & \;\;\;\;\;\text{"extract common parts: $\;\dots \min (x+y)\;$, $\;(-x -y) \min \dots\;$"} \\ & (((x - y) \;\max\; (y - x)) \min (x + y)) \;\max\; \\ & ((-x - y) \min ((y - x) \;\max\; (x - y))) \\ = & \;\;\;\;\;\text{"extract common part: $\;((x - y) \;\max\; (y - x)) \min \dots\;$"} \\ & ((x - y) \max (y - x)) \;\min\; ((x + y) \max (-x - y)) \\ = & \;\;\;\;\;\text{"definition $(0)$, twice"} \\ & |x - y| \;\min\; |x + y| \\ \leq & \;\;\;\;\;\text{"$\;p \min q \leq p\;$"} \\ & |x - y| \\ \end{align} which completes this proof.