An exact proof term for the current goal is nat_p_ordinal 2 nat_2.