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.
Apply SNoLt_trichotomy_or_impred (recip_SNo_pos x) 0 Lrx SNo_0 to the current goal.
Assume H1: recip_SNo_pos x < 0.
We will prove False.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
Apply SNoLt_tra 0 1 0 SNo_0 SNo_1 SNo_0 SNoLt_0_1 to the current goal.
We will prove 1 < 0.
rewrite the current goal using recip_SNo_pos_invR x Hx Hxpos (from right to left).
We will prove x * recip_SNo_pos x < 0.
An exact proof term for the current goal is mul_SNo_pos_neg x (recip_SNo_pos x) Hx Lrx Hxpos H1.
Assume H1: recip_SNo_pos x = 0.
We will prove False.
Apply neq_1_0 to the current goal.
We will prove 1 = 0.
rewrite the current goal using recip_SNo_pos_invR x Hx Hxpos (from right to left).
We will prove x * recip_SNo_pos x = 0.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is mul_SNo_zeroR x Hx.
Assume H1.
An exact proof term for the current goal is H1.
∎