Let n be given.
Assume HnS: SNo n.
We will prove div_SNo 1 n = inv_nat n.
We prove the intermediate claim Hdivdef: div_SNo 1 n = mul_SNo 1 (recip_SNo n).
Use reflexivity.
rewrite the current goal using Hdivdef (from left to right).
rewrite the current goal using (mul_SNo_oneL (recip_SNo n) (SNo_recip_SNo n HnS)) (from left to right).
We prove the intermediate claim Hinvdef: inv_nat n = recip_SNo n.
Use reflexivity.
rewrite the current goal using Hinvdef (from left to right).
Use reflexivity.
∎