Let x, y and z be given.
Assume Hx Hxnp Hy Hz Hzy.
Apply SNoLtLe_or x 0 Hx SNo_0 to the current goal.
Assume H1: x < 0.
Apply SNoLtLe_or z y Hz Hy to the current goal.
Assume H2: z < y.
Apply SNoLtLe to the current goal.
We will prove x * y < x * z.
An exact proof term for the current goal is neg_mul_SNo_Lt x y z Hx H1 Hy Hz H2.
Assume H2: y ≤ z.
We prove the intermediate claim L1: y = z.
Apply SNoLe_antisym y z Hy Hz to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is Hzy.
rewrite the current goal using L1 (from left to right).
Apply SNoLe_ref to the current goal.
Assume H1: 0 ≤ x.
We prove the intermediate claim L1: x = 0.
Apply SNoLe_antisym x 0 Hx SNo_0 to the current goal.
An exact proof term for the current goal is Hxnp.
An exact proof term for the current goal is H1.
rewrite the current goal using L1 (from left to right).
We will prove 0 * y ≤ 0 * z.
rewrite the current goal using mul_SNo_zeroL y Hy (from left to right).
rewrite the current goal using mul_SNo_zeroL z Hz (from left to right).
Apply SNoLe_ref to the current goal.
∎