Apply int_SNo_cases to the current goal.

An exact proof term for the current goal is omega_SNo.

Let n be given.

Assume Hn.

We will prove SNo (- n).

Apply SNo_minus_SNo to the current goal.

We will prove SNo n.

An exact proof term for the current goal is omega_SNo n Hn.

∎