Let α be given.

Assume Ha.

Apply ordinal_In_SNoLt (ordsucc α) (ordinal_ordsucc α Ha) 0 to the current goal.

We will prove 0 ∈ ordsucc α.

An exact proof term for the current goal is ordinal_0_In_ordsucc α Ha.

∎