An exact proof term for the current goal is If_i_1 (0 < x) (recip_SNo_pos x) (if x < 0 then - recip_SNo_pos (- x) else 0) Hxpos.