An exact proof term for the current goal is (ordsucc_inj_contra 0 1 neq_0_1).