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