Let n be given.

Assume Hn.

Apply nat_p_SNo to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hn.

∎