An exact proof term for the current goal is ordinal_SNoR 1 (nat_p_ordinal 1 nat_1).