Let x be given.

Assume HxS: SNo x.

Assume Hpos: 0 < x.

Assume Heq: x = 0.

We prove the intermediate claim H00: 0 < 0.

rewrite the current goal using Heq (from right to left) at position 2.

An exact proof term for the current goal is Hpos.

An exact proof term for the current goal is ((SNoLt_irref 0) H00).

∎