Let x, y and z be given.

Assume Hx Hy Hz Hypos.

Assume H1: x < z * y.

We will prove x :/: y < z.

rewrite the current goal using mul_SNo_oneR z Hz (from right to left).

We will prove x :/: y < z * 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_invR y Hy Ly0 (from right to left).

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

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

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

Apply pos_mul_SNo_Lt' x (z * y) (recip_SNo y) Hx (SNo_mul_SNo z y Hz Hy) (SNo_recip_SNo y Hy) to the current goal.

We will prove 0 < recip_SNo y.

An exact proof term for the current goal is recip_SNo_of_pos_is_pos y Hy Hypos.

We will prove x < z * y.

An exact proof term for the current goal is H1.

∎