Let p and q be given.
Apply ordinal_ind to the current goal.
Let alpha be given.
Assume Ha.
Assume IH: ∀beta ∈ alpha, PNoLt_ beta p q ∨ PNoEq_ beta p q ∨ PNoLt_ beta q p.
Apply xm (PNoEq_ alpha p q) to the current goal.
Assume H1: PNoEq_ alpha p q.
Apply orIL to the current goal.
Apply orIR to the current goal.
An exact proof term for the current goal is H1.
Assume H1: ¬ PNoEq_ alpha p q.
We prove the intermediate claim L1: ∃beta, ¬ (beta ∈ alpha → (p beta ↔ q beta)).
An exact proof term for the current goal is not_all_ex_demorgan_i (λbeta ⇒ beta ∈ alpha → (p beta ↔ q beta)) H1.
Apply L1 to the current goal.
Let beta be given.
Assume H2: ¬ (beta ∈ alpha → (p beta ↔ q beta)).
We prove the intermediate claim L2: beta ∈ alpha ∧ ¬ (p beta ↔ q beta).
Apply xm (beta ∈ alpha) to the current goal.
Assume H3: beta ∈ alpha.
Apply xm (p beta ↔ q beta) to the current goal.
Assume H4: p beta ↔ q beta.
We will prove False.
Apply H2 to the current goal.
Assume _.
An exact proof term for the current goal is H4.
Assume H4: ¬ (p beta ↔ q beta).
Apply andI to the current goal.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is H4.
Assume H3: beta ∉ alpha.
We will prove False.
Apply H2 to the current goal.
Assume H4.
We will prove False.
An exact proof term for the current goal is H3 H4.
Apply L2 to the current goal.
Assume H3: beta ∈ alpha.
Assume H4: ¬ (p beta ↔ q beta).
Apply IH beta H3 to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: PNoLt_ beta p q.
Apply orIL to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is PNoLt_mon_ p q alpha Ha beta H3 H5.
Assume H5: PNoEq_ beta p q.
Apply xm (p beta) to the current goal.
Assume H6: p beta.
Apply xm (q beta) to the current goal.
Assume H7: q beta.
We will prove False.
Apply H4 to the current goal.
Apply iffI to the current goal.
Assume _.
An exact proof term for the current goal is H7.
Assume _.
An exact proof term for the current goal is H6.
Assume H7: ¬ q beta.
Apply orIR to the current goal.
We will prove ∃beta ∈ alpha, PNoEq_ beta q p ∧ ¬ q beta ∧ p beta.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
Apply and3I to the current goal.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H7.
An exact proof term for the current goal is H6.
Assume H6: ¬ p beta.
Apply xm (q beta) to the current goal.
Assume H7: q beta.
Apply orIL to the current goal.
Apply orIL to the current goal.
We will prove ∃beta ∈ alpha, PNoEq_ beta p q ∧ ¬ p beta ∧ q beta.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3.
Apply and3I to the current goal.
An exact proof term for the current goal is H5.
An exact proof term for the current goal is H6.
An exact proof term for the current goal is H7.
Assume H7: ¬ q beta.
We will prove False.
Apply H4 to the current goal.
Apply iffI to the current goal.
Assume H8.
We will prove False.
An exact proof term for the current goal is H6 H8.
Assume H8.
We will prove False.
An exact proof term for the current goal is H7 H8.
Assume H5: PNoLt_ beta q p.
Apply orIR to the current goal.
An exact proof term for the current goal is PNoLt_mon_ q p alpha Ha beta H3 H5.
∎