Let x, y and z be given.
Assume Hx Hy Hz H1.
We prove the intermediate
claim L1:
(x + y) + - y = x.
We prove the intermediate
claim L2:
(z + y) + - y = z.
rewrite the current goal using L1 (from right to left).
rewrite the current goal using L2 (from right to left).
We will
prove (x + y) + - y ≤ (z + y) + - y.
∎