Let α and β be given.
Assume Ha Hb Hab.
We prove the intermediate claim L1: α ordsucc β.
Apply ordinal_In_Or_Subq α β Ha Hb to the current goal.
Assume H1: α β.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H1.
Assume H1: β α.
We prove the intermediate claim L1a: α = β.
Apply set_ext to the current goal.
An exact proof term for the current goal is Hab.
An exact proof term for the current goal is H1.
rewrite the current goal using L1a (from left to right).
Apply ordsuccI2 to the current goal.
We prove the intermediate claim La1: SNo α.
An exact proof term for the current goal is ordinal_SNo α Ha.
We prove the intermediate claim La2: SNoLev α = α.
An exact proof term for the current goal is ordinal_SNoLev α Ha.
Apply ordinal_SNoLev_max_2 β Hb α La1 to the current goal.
We will prove SNoLev α ordsucc β.
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is L1.