Apply nat_ind to the current goal.

We will prove ordinal 0.

An exact proof term for the current goal is ordinal_Empty.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: ordinal n.

We will prove ordinal (ordsucc n).

An exact proof term for the current goal is (ordinal_ordsucc n IHn).

∎