Let x, y, z and w be given.
Assume Hx Hy Hz Hw Hxpos Hypos Hxz Hyw.
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.
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.
∎