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 add_SNo_Lt3a x y z w Hx Hy Hz Hw Hxz to the current goal.

We will prove y ≤ w.

Apply SNoLtLe to the current goal.

We will prove y < w.

An exact proof term for the current goal is Hyw.

∎