Let α and β be given.

Assume Ha Hb.

We prove the intermediate claim L1: ordinal (ordsucc β).

An exact proof term for the current goal is ordinal_ordsucc β (ordinal_Hered α Ha β Hb).

Apply ordinal_trichotomy_or α (ordsucc β) Ha L1 to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H2: α ∈ ordsucc β.

We will prove False.

Apply ordsuccE β α H2 to the current goal.

Assume H3: α ∈ β.

An exact proof term for the current goal is In_no2cycle α β H3 Hb.

Assume H3: α = β.

Apply In_irref α to the current goal.

rewrite the current goal using H3 (from left to right) at position 1.

An exact proof term for the current goal is Hb.

Assume H2: α = ordsucc β.

Apply orIR to the current goal.

An exact proof term for the current goal is H2.

Assume H2: ordsucc β ∈ α.

Apply orIL to the current goal.

An exact proof term for the current goal is H2.

∎