Let x and y be given.

Assume Hx Hy Hx1 Hy0.

rewrite the current goal using mul_SNo_oneL y Hy (from right to left) at position 2.

We will prove x * y < 1 * y.

An exact proof term for the current goal is pos_mul_SNo_Lt' x 1 y Hx SNo_1 Hy Hy0 Hx1.

∎