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