Apply ordinal_SNo to the current goal.

Apply nat_p_ordinal to the current goal.

An exact proof term for the current goal is nat_1.

∎