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 SNoLeLt_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_Le1 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_Lt2 z y w Hz Hy Hw Hyw.

∎