Let x, y, z and w be given.
Assume Hx Hy Hz Hw Hxpos Hypos Hxz Hyw.
Apply SNoLt_tra (x * y) (x * w) (z * w) (SNo_mul_SNo x y Hx Hy) (SNo_mul_SNo x w Hx Hw) (SNo_mul_SNo z w Hz Hw) to the current goal.
We will prove x * y < x * w.
An exact proof term for the current goal is pos_mul_SNo_Lt x y w Hx Hxpos Hy Hw Hyw.
We will prove x * w < z * w.
Apply pos_mul_SNo_Lt' x z w Hx Hz Hw to the current goal.
We will prove 0 < w.
An exact proof term for the current goal is SNoLt_tra 0 y w SNo_0 Hy Hw Hypos Hyw.
An exact proof term for the current goal is Hxz.
∎