An exact proof term for the current goal is (neq_0_ordsucc 1).