Let x and y be given.

Assume Hx Hy Hxpos Hypos.

We will prove 0 < x * recip_SNo y.

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

∎