Let x be given.
Assume Hx Hxneg.
We prove the intermediate claim L1: ¬ (0 < x).
Assume H1.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
An exact proof term for the current goal is SNoLt_tra 0 x 0 SNo_0 Hx SNo_0 H1 Hxneg.
We will prove (if 0 < x then recip_SNo_pos x else if x < 0 then - recip_SNo_pos (- x) else 0) = - recip_SNo_pos (- x).
rewrite the current goal using If_i_0 (0 < x) (recip_SNo_pos x) (if x < 0 then - recip_SNo_pos (- x) else 0) L1 (from left to right).
An exact proof term for the current goal is If_i_1 (x < 0) (- recip_SNo_pos (- x)) 0 Hxneg.
∎