Let alpha be given.
Assume Ha.
Let p, q and r be given.
Assume Hpq Hqr.
We will prove ∃beta ∈ alpha, PNoEq_ beta p r ∧ ¬ p beta ∧ r beta.
Apply PNoLt_E_ alpha p q Hpq to the current goal.
Let beta be given.
Assume Hbeta1: beta ∈ alpha.
Assume Hbeta2: PNoEq_ beta p q.
Assume Hbeta3: ¬ p beta.
Assume Hbeta4: q beta.
Apply PNoLt_E_ alpha q r Hqr to the current goal.
Let gamma be given.
Assume Hgamma1: gamma ∈ alpha.
Assume Hgamma2: PNoEq_ gamma q r.
Assume Hgamma3: ¬ q gamma.
Assume Hgamma4: r gamma.
We prove the intermediate claim Lbeta: ordinal beta.
An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hbeta1.
We prove the intermediate claim Lgamma: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered alpha Ha gamma Hgamma1.
Apply ordinal_trichotomy_or beta gamma Lbeta Lgamma to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: beta ∈ gamma.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hbeta1.
Apply and3I to the current goal.
We will prove PNoEq_ beta p r.
Apply PNoEq_tra_ beta p q r Hbeta2 to the current goal.
We will prove PNoEq_ beta q r.
An exact proof term for the current goal is PNoEq_antimon_ q r gamma Lgamma beta H1 Hgamma2.
We will prove ¬ p beta.
An exact proof term for the current goal is Hbeta3.
We will prove r beta.
Apply Hgamma2 beta H1 to the current goal.
Assume H2 _.
An exact proof term for the current goal is H2 Hbeta4.
Assume H1: beta = gamma.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hbeta1.
Apply and3I to the current goal.
We will prove PNoEq_ beta p r.
Apply PNoEq_tra_ beta p q r Hbeta2 to the current goal.
We will prove PNoEq_ beta q r.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hgamma2.
We will prove ¬ p beta.
An exact proof term for the current goal is Hbeta3.
We will prove r beta.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hgamma4.
Assume H1: gamma ∈ beta.
We use gamma to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hgamma1.
Apply and3I to the current goal.
We will prove PNoEq_ gamma p r.
Apply PNoEq_tra_ gamma p q r to the current goal.
We will prove PNoEq_ gamma p q.
An exact proof term for the current goal is PNoEq_antimon_ p q beta Lbeta gamma H1 Hbeta2.
An exact proof term for the current goal is Hgamma2.
We will prove ¬ p gamma.
Assume H2: p gamma.
Apply Hbeta2 gamma H1 to the current goal.
Assume H3 _.
Apply Hgamma3 to the current goal.
We will prove q gamma.
An exact proof term for the current goal is H3 H2.
We will prove r gamma.
An exact proof term for the current goal is Hgamma4.
∎