We will prove (if 0 < 0 then recip_SNo_pos 0 else if 0 < 0 then - recip_SNo_pos (- 0) else 0) = 0.

rewrite the current goal using If_i_0 (0 < 0) (recip_SNo_pos 0) (if 0 < 0 then - recip_SNo_pos (- 0) else 0) (SNoLt_irref 0) (from left to right).

We will prove (if 0 < 0 then - recip_SNo_pos (- 0) else 0) = 0.

An exact proof term for the current goal is If_i_0 (0 < 0) (- recip_SNo_pos (- 0)) 0 (SNoLt_irref 0).

∎