Let x and y be given.

Assume Hx Hy Hx0 Hy0.

We will prove 0 < x * y.

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

We will prove 0 + 0 < x * y.

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

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

rewrite the current goal using mul_SNo_zeroR 0 SNo_0 (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 y Hy (from right to left) at position 1.

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

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

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

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

∎