Let x, y and z be given.

Assume Hx Hy Hz Hypos.

Assume H1: z < x :/: y.

We will prove z * y < x.

rewrite the current goal using mul_SNo_oneR x Hx (from right to left).

We will prove z * y < x * 1.

We prove the intermediate claim Ly0: y ≠ 0.

Assume H2: y = 0.

Apply SNoLt_irref y to the current goal.

We will prove y < y.

rewrite the current goal using H2 (from left to right) at position 1.

An exact proof term for the current goal is Hypos.

rewrite the current goal using recip_SNo_invL y Hy Ly0 (from right to left).

We will prove z * y < x * (recip_SNo y * y).

rewrite the current goal using mul_SNo_assoc x (recip_SNo y) y Hx (SNo_recip_SNo y Hy) Hy (from left to right).

We will prove z * y < (x * recip_SNo y) * y.

We will prove z * y < (x :/: y) * y.

An exact proof term for the current goal is pos_mul_SNo_Lt' z (x :/: y) y Hz (SNo_div_SNo x y Hx Hy) Hy Hypos H1.

∎