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