Let x, y, z, w and u be given.

Assume Hx Hy Hz Hw Hu H1.

rewrite the current goal using add_SNo_assoc x y u Hx Hy Hu (from left to right).

rewrite the current goal using add_SNo_assoc z w u Hz Hw Hu (from left to right).

We will prove (x + y) + u < (z + w) + u.

An exact proof term for the current goal is add_SNo_Lt1 (x + y) u (z + w) (SNo_add_SNo x y Hx Hy) Hu (SNo_add_SNo z w Hz Hw) H1.

∎