Let x, y and z be given.

Assume Hx Hy Hz Hypos.

Assume H1: x :/: y < z.

We will prove x < z * y.

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

We will prove x * 1 < z * y.

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 x * (recip_SNo y * y) < z * 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 (x * recip_SNo y) * y < z * y.

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

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

∎