Let x and y be given.

Assume Hx Hy.

We will prove SNo (x * recip_SNo y).

An exact proof term for the current goal is SNo_mul_SNo x (recip_SNo y) Hx (SNo_recip_SNo y Hy).

∎