Let x and y be given.

Assume Hx Hy Hx1 Hy0.

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

We will prove x * y ≤ 1 * y.

An exact proof term for the current goal is nonneg_mul_SNo_Le' x 1 y Hx SNo_1 Hy Hy0 Hx1.

∎