Assume H1: x < 0.

Apply SNoLtLe to the current goal.

We will prove 0 < x * y.

An exact proof term for the current goal is mul_SNo_neg_neg x y Hx Hy H1 Hyneg.

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 ≤ 0 * y.

rewrite the current goal using mul_SNo_zeroL y Hy (from left to right).

Apply SNoLe_ref to the current goal.