Let x, y, z, u, v and w be given.
Assume Hx Hy Hz Hu Hv Hw H1.
We prove the intermediate claim Lmz: SNo (- z).
An exact proof term for the current goal is SNo_minus_SNo z Hz.
We prove the intermediate claim Lmw: SNo (- w).
An exact proof term for the current goal is SNo_minus_SNo w Hw.
We prove the intermediate claim Lxy: SNo (x + y).
An exact proof term for the current goal is SNo_add_SNo x y Hx Hy.
We prove the intermediate claim Luv: SNo (u + v).
An exact proof term for the current goal is SNo_add_SNo u v Hu Hv.
rewrite the current goal using add_SNo_assoc x y (- z) Hx Hy Lmz (from left to right).
rewrite the current goal using add_SNo_assoc u v (- w) Hu Hv Lmw (from left to right).
We will prove (x + y) + - z < (u + v) + - w.
Apply add_SNo_minus_Lt2b (u + v) w ((x + y) + - z) Luv Hw (SNo_add_SNo (x + y) (- z) Lxy Lmz) to the current goal.
We will prove ((x + y) + - z) + w < u + v.
rewrite the current goal using add_SNo_assoc (x + y) (- z) w Lxy Lmz Hw (from right to left).
We will prove (x + y) + - z + w < u + v.
rewrite the current goal using add_SNo_com (- z) w Lmz Hw (from left to right).
We will prove (x + y) + w + - z < u + v.
rewrite the current goal using add_SNo_assoc (x + y) w (- z) Lxy Hw Lmz (from left to right).
We will prove ((x + y) + w) + - z < u + v.
Apply add_SNo_minus_Lt1b ((x + y) + w) z (u + v) (SNo_add_SNo (x + y) w Lxy Hw) Hz Luv to the current goal.
We will prove (x + y) + w < (u + v) + z.
rewrite the current goal using add_SNo_assoc x y w Hx Hy Hw (from right to left).
rewrite the current goal using add_SNo_assoc u v z Hu Hv Hz (from right to left).
An exact proof term for the current goal is H1.
∎