Let n be given.

Assume Hn.

Apply ordinal_SNo to the current goal.

We will prove ordinal n.

Apply nat_p_ordinal to the current goal.

An exact proof term for the current goal is Hn.

∎