Let x and y be given.

Assume Hx Hy Hy0.

We will prove (x * recip_SNo y) * y = x.

rewrite the current goal using mul_SNo_assoc x (recip_SNo y) y Hx (SNo_recip_SNo y Hy) Hy (from right to left).

We will prove x * (recip_SNo y * y) = x.

rewrite the current goal using recip_SNo_invL y Hy Hy0 (from left to right).

We will prove x * 1 = x.

An exact proof term for the current goal is mul_SNo_oneR x Hx.

∎