Apply mul_SNo_nonzero_cancel 1 (recip_SNo_pos 1) 1 SNo_1 neq_1_0 (SNo_recip_SNo_pos 1 SNo_1 SNoLt_0_1) SNo_1 to the current goal.

We will prove 1 * recip_SNo_pos 1 = 1 * 1.

rewrite the current goal using mul_SNo_oneL 1 SNo_1 (from left to right).

We will prove 1 * recip_SNo_pos 1 = 1.

An exact proof term for the current goal is recip_SNo_pos_invR 1 SNo_1 SNoLt_0_1.

∎