Let x and y be given.

Assume Hx Hy Hxneg Hyneg.

We will prove 0 < x * recip_SNo y.

Apply mul_SNo_neg_neg x (recip_SNo y) Hx (SNo_recip_SNo y Hy) Hxneg 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.

∎