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.