An exact proof term for the current goal is (ordsuccI2 0).