Let x and y be given.
Assume Hx Hy Hxnp Hynn.
Apply SNoLeE 0 y SNo_0 Hy Hynn to the current goal.
Assume H1: 0 < y.
An exact proof term for the current goal is mul_SNo_nonpos_pos x y Hx Hy Hxnp H1.
Assume H1: 0 = y.
rewrite the current goal using H1 (from right to left).
We will prove x * 0 ≤ 0.
rewrite the current goal using mul_SNo_zeroR x Hx (from left to right).
Apply SNoLe_ref to the current goal.
∎