We will prove inv_nat 1 = 1.

We prove the intermediate claim H1neq0: 1 ≠ 0.

An exact proof term for the current goal is neq_1_0.

We prove the intermediate claim Hmul: mul_SNo 1 (inv_nat 1) = 1.

An exact proof term for the current goal is (recip_SNo_invR 1 SNo_1 H1neq0).

rewrite the current goal using (mul_SNo_oneL (inv_nat 1) (SNo_recip_SNo 1 SNo_1)) (from right to left) at position 1.

An exact proof term for the current goal is Hmul.

∎