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.