Let x, y and z be given.
Assume Hx Hxn0 Hy Hz Hxyz.
Apply SNoLt_trichotomy_or_impred y z Hy Hz to the current goal.
Assume H1: y < z.
We will prove False.
Apply SNoLt_trichotomy_or_impred x 0 Hx SNo_0 to the current goal.
Assume H2: x < 0.
Apply SNoLt_irref (x * y) to the current goal.
We will prove x * y < x * y.
rewrite the current goal using Hxyz (from left to right) at position 1.
We will prove x * z < x * y.
An exact proof term for the current goal is neg_mul_SNo_Lt x z y Hx H2 Hz Hy H1.
Assume H2: x = 0.
An exact proof term for the current goal is Hxn0 H2.
Assume H2: 0 < x.
Apply SNoLt_irref (x * y) to the current goal.
We will prove x * y < x * y.
rewrite the current goal using Hxyz (from left to right) at position 2.
We will prove x * y < x * z.
An exact proof term for the current goal is pos_mul_SNo_Lt x y z Hx H2 Hy Hz H1.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1: z < y.
We will prove False.
Apply SNoLt_trichotomy_or_impred x 0 Hx SNo_0 to the current goal.
Assume H2: x < 0.
Apply SNoLt_irref (x * y) to the current goal.
We will prove x * y < x * y.
rewrite the current goal using Hxyz (from left to right) at position 2.
We will prove x * y < x * z.
An exact proof term for the current goal is neg_mul_SNo_Lt x y z Hx H2 Hy Hz H1.
Assume H2: x = 0.
An exact proof term for the current goal is Hxn0 H2.
Assume H2: 0 < x.
Apply SNoLt_irref (x * y) to the current goal.
We will prove x * y < x * y.
rewrite the current goal using Hxyz (from left to right) at position 1.
We will prove x * z < x * y.
An exact proof term for the current goal is pos_mul_SNo_Lt x z y Hx H2 Hz Hy H1.
∎