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_0R (x * y) (SNo_mul_SNo x y Hx Hy) (from right to left).

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

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

rewrite the current goal using mul_SNo_zeroR y Hy (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 x * y + 0 * 0 < 0 * y + x * 0.

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

∎