Let x, y and z be given.

Assume Hx Hy Hz Hypos.

Assume H1: z * y < x.

We will prove z < x :/: y.

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

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

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

Apply pos_mul_SNo_Lt' (z * y) x (recip_SNo y) (SNo_mul_SNo z y Hz Hy) Hx (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 z * y < x.

An exact proof term for the current goal is H1.

∎