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.
∎