Apply ordsucc_inj_contra to the current goal.

An exact proof term for the current goal is neq_1_3.

∎