Let x, y, z, w, u and v be given.
Assume Hx Hy Hz Hw Hu Hv.
Assume H1: x + y + v ≤ w + u + z.
We will prove x + y + - z ≤ w + u + - v.
We prove the intermediate claim Lmv: SNo (- v).
An exact proof term for the current goal is SNo_minus_SNo v Hv.
Apply add_SNo_minus_Le1b3 x y z (w + u + - v) Hx Hy Hz (SNo_add_SNo_3 w u (- v) Hw Hu Lmv) to the current goal.
We will prove x + y ≤ (w + u + - v) + z.
rewrite the current goal using add_SNo_assoc w u (- v) Hw Hu Lmv (from left to right).
We will prove x + y ≤ ((w + u) + - v) + z.
rewrite the current goal using add_SNo_com_3b_1_2 (w + u) (- v) z (SNo_add_SNo w u Hw Hu) Lmv Hz (from left to right).
We will prove x + y ≤ ((w + u) + z) + - v.
Apply add_SNo_minus_Le2b ((w + u) + z) v (x + y) (SNo_add_SNo (w + u) z (SNo_add_SNo w u Hw Hu) Hz) Hv (SNo_add_SNo x y Hx Hy) to the current goal.
We will prove (x + y) + v ≤ (w + u) + z.
rewrite the current goal using add_SNo_assoc x y v Hx Hy Hv (from right to left).
rewrite the current goal using add_SNo_assoc w u z Hw Hu Hz (from right to left).
An exact proof term for the current goal is H1.
∎