Let x be given.

Assume Hx: SNo x.

We prove the intermediate claim Lmx: SNo (- x).

An exact proof term for the current goal is SNo_minus_SNo x Hx.

We will prove x + - x = 0.

rewrite the current goal using add_SNo_com x (- x) Hx Lmx (from left to right).

We will prove - x + x = 0.

An exact proof term for the current goal is add_SNo_minus_SNo_linv x Hx.

∎