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