Let x be given.
Assume Hx Hxpos.
We prove the intermediate claim Lrx: SNo (recip_SNo_pos x).
An exact proof term for the current goal is SNo_recip_SNo_pos x Hx Hxpos.
We prove the intermediate claim Lrxpos: 0 < recip_SNo_pos x.
An exact proof term for the current goal is recip_SNo_pos_is_pos x Hx Hxpos.
We prove the intermediate claim Lrrx: SNo (recip_SNo_pos (recip_SNo_pos x)).
An exact proof term for the current goal is SNo_recip_SNo_pos (recip_SNo_pos x) Lrx Lrxpos.
We prove the intermediate claim Lrxn0: recip_SNo_pos x ≠ 0.
Assume Hrx0: recip_SNo_pos x = 0.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using Hrx0 (from right to left) at position 2.
An exact proof term for the current goal is Lrxpos.
We will prove recip_SNo_pos (recip_SNo_pos x) = x.
Apply mul_SNo_nonzero_cancel (recip_SNo_pos x) (recip_SNo_pos (recip_SNo_pos x)) x Lrx Lrxn0 Lrrx Hx to the current goal.
We will prove recip_SNo_pos x * recip_SNo_pos (recip_SNo_pos x) = recip_SNo_pos x * x.
rewrite the current goal using mul_SNo_com (recip_SNo_pos x) x Lrx Hx (from left to right).
rewrite the current goal using recip_SNo_pos_invR x Hx Hxpos (from left to right).
An exact proof term for the current goal is recip_SNo_pos_invR (recip_SNo_pos x) Lrx Lrxpos.
∎