Apply ordsucc_inj_contra to the current goal.

An exact proof term for the current goal is neq_2_3.

∎