Let x and y be given.

Assume Hx Hy Hx0 Hy0.

We will prove x * y < 0.

rewrite the current goal using add_SNo_0R 0 SNo_0 (from right to left).

rewrite the current goal using add_SNo_0L (x * y) (SNo_mul_SNo x y Hx Hy) (from right to left).

We will prove 0 + x * y < 0 + 0.

rewrite the current goal using mul_SNo_zeroR y Hy (from right to left) at position 3.

rewrite the current goal using mul_SNo_zeroR x Hx (from right to left) at position 2.

rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (from right to left) at position 1.

rewrite the current goal using mul_SNo_com y 0 Hy SNo_0 (from left to right).

We will prove 0 * 0 + x * y < x * 0 + 0 * y.

An exact proof term for the current goal is mul_SNo_Lt x 0 0 y Hx SNo_0 SNo_0 Hy Hx0 Hy0.

∎