Let x and y be given.

Assume Hx Hy Hxneg Hypos.

We will prove x * recip_SNo y < 0.

Apply mul_SNo_neg_pos x (recip_SNo y) Hx (SNo_recip_SNo y Hy) Hxneg to the current goal.

We will prove 0 < recip_SNo y.

An exact proof term for the current goal is recip_SNo_of_pos_is_pos y Hy Hypos.

∎