Let x and y be given.

Assume Hx Hy Hxpos Hyneg.

We will prove x * recip_SNo y < 0.

Apply mul_SNo_pos_neg x (recip_SNo y) Hx (SNo_recip_SNo y Hy) Hxpos to the current goal.

We will prove recip_SNo y < 0.

An exact proof term for the current goal is recip_SNo_neg' y Hy Hyneg.

∎