Let x and y be given.
Assume Hx Hy Hxnn Hynn.
Apply SNoLeE 0 x SNo_0 Hx Hxnn to the current goal.
Assume H1: 0 < x.
Apply SNoLeE 0 y SNo_0 Hy Hynn to the current goal.
Assume H2: 0 < y.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is mul_SNo_pos_pos x y Hx Hy H1 H2.
Assume H2: 0 = y.
rewrite the current goal using H2 (from right to left).
rewrite the current goal using mul_SNo_zeroR x Hx (from left to right).
Apply SNoLe_ref to the current goal.
Assume H1: 0 = x.
rewrite the current goal using H1 (from right to left).
rewrite the current goal using mul_SNo_zeroL y Hy (from left to right).
Apply SNoLe_ref to the current goal.
∎