Let x, y, z and w be given.

Assume Hx: SNo x.

Assume Hy: SNo y.

Assume Hz: SNo z.

Assume Hw: SNo w.

Assume Hxz: x < z.

Assume Hyw: y ≤ w.

Apply SNoLtLe_tra (x + y) (z + y) (z + w) (SNo_add_SNo x y Hx Hy) (SNo_add_SNo z y Hz Hy) (SNo_add_SNo z w Hz Hw) to the current goal.

We will prove x + y < z + y.

An exact proof term for the current goal is add_SNo_Lt1 x y z Hx Hy Hz Hxz.

We will prove z + y ≤ z + w.

An exact proof term for the current goal is add_SNo_Le2 z y w Hz Hy Hw Hyw.

∎