Let a and b be given.

Assume H1.

We will prove ¬ (ordsucc a = ordsucc b).

Assume H2: ordsucc a = ordsucc b.

An exact proof term for the current goal is H1 (ordsucc_inj a b H2).

∎