Let alpha be given.
Assume Ha.
Apply xm (∃beta ∈ alpha, alpha = ordsucc beta) to the current goal.
Assume H1.
Apply orIR to the current goal.
An exact proof term for the current goal is H1.
Assume H1: ¬ ∃beta ∈ alpha, alpha = ordsucc beta.
Apply orIL to the current goal.
Let beta be given.
Assume H2: beta ∈ alpha.
Apply ordinal_ordsucc_In_eq alpha beta Ha H2 to the current goal.
Assume H3: ordsucc beta ∈ alpha.
An exact proof term for the current goal is H3.
Assume H3: alpha = ordsucc beta.
We will prove False.
Apply H1 to the current goal.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H3.
∎