Let n be given.

Assume Hn.

Apply nat_p_omega to the current goal.

Apply nat_ordsucc to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hn.

∎