Let alpha, beta and gamma be given.
Assume Ha Hb Hc.
Apply Ha to the current goal.
Assume Ha1 _.
Apply Hc to the current goal.
Assume Hc1 _.
Let p, q and r be given.
Assume Hpq Hqr.
Apply PNoLtE alpha beta p q Hpq to the current goal.
Assume Hpq1: PNoLt_ (alpha ∩ beta) p q.
Apply Hpq1 to the current goal.
Let delta be given.
Assume Hpq2.
Apply Hpq2 to the current goal.
Assume Hd: delta ∈ alpha ∩ beta.
Apply binintersectE alpha beta delta Hd to the current goal.
Assume Hd1 Hd2.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3.
Apply Hpq3 to the current goal.
Assume Hpq3: PNoEq_ delta p q.
Assume Hpq4: ¬ p delta.
Assume Hpq5: q delta.
We prove the intermediate claim Ld: ordinal delta.
An exact proof term for the current goal is ordinal_Hered beta Hb delta Hd2.
Apply PNoLtE beta gamma q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (beta ∩ gamma) q r.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume He: eps ∈ beta ∩ gamma.
Apply binintersectE beta gamma eps He to the current goal.
Assume He1 He2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ eps q r.
Assume Hqr4: ¬ q eps.
Assume Hqr5: r eps.
We prove the intermediate claim Le: ordinal eps.
An exact proof term for the current goal is ordinal_Hered beta Hb eps He1.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
Apply ordinal_trichotomy_or delta eps Ld Le to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: delta ∈ eps.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove delta ∈ gamma.
An exact proof term for the current goal is Hc1 eps He2 delta H1.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
Apply PNoEq_antimon_ q r eps Le delta H1 to the current goal.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
An exact proof term for the current goal is iffEL (q delta) (r delta) (Hqr3 delta H1) Hpq5.
Assume H1: delta = eps.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove delta ∈ gamma.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr3.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr5.
Assume H1: eps ∈ delta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
We will prove eps ∈ alpha.
An exact proof term for the current goal is Ha1 delta Hd1 eps H1.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p q r to the current goal.
We will prove PNoEq_ eps p q.
Apply PNoEq_antimon_ p q delta Ld eps H1 to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p eps.
Assume H2: p eps.
Apply Hqr4 to the current goal.
An exact proof term for the current goal is iffEL (p eps) (q eps) (Hpq3 eps H1) H2.
We will prove r eps.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: beta ∈ gamma.
Assume Hqr2: PNoEq_ beta q r.
Assume Hqr3: r beta.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove delta ∈ gamma.
An exact proof term for the current goal is Hc1 beta Hqr1 delta Hd2.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
Apply PNoEq_antimon_ q r beta Hb delta Hd2 to the current goal.
We will prove PNoEq_ beta q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
An exact proof term for the current goal is iffEL (q delta) (r delta) (Hqr2 delta Hd2) Hpq5.
Assume Hqr1: gamma ∈ beta.
Assume Hqr2: PNoEq_ gamma q r.
Assume Hqr3: ¬ q gamma.
Apply ordinal_trichotomy_or delta gamma Ld Hc to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: delta ∈ gamma.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hd1.
We will prove delta ∈ gamma.
An exact proof term for the current goal is H1.
Apply and3I to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p q r to the current goal.
We will prove PNoEq_ delta p q.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ delta q r.
Apply PNoEq_antimon_ q r gamma Hc delta H1 to the current goal.
We will prove PNoEq_ gamma q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p delta.
An exact proof term for the current goal is Hpq4.
We will prove r delta.
An exact proof term for the current goal is iffEL (q delta) (r delta) (Hqr2 delta H1) Hpq5.
Assume H1: delta = gamma.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hd1.
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.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ gamma q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p gamma.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq4.
Assume H1: gamma ∈ delta.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Ha1 delta Hd1 gamma H1.
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.
Apply PNoEq_antimon_ p q delta Ld gamma H1 to the current goal.
An exact proof term for the current goal is Hpq3.
We will prove PNoEq_ gamma q r.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p gamma.
Assume H2: p gamma.
Apply Hqr3 to the current goal.
We will prove q gamma.
An exact proof term for the current goal is iffEL (p gamma) (q gamma) (Hpq3 gamma H1) H2.
Assume Hpq1: alpha ∈ beta.
Assume Hpq2: PNoEq_ alpha p q.
Assume Hpq3: q alpha.
Apply PNoLtE beta gamma q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (beta ∩ gamma) q r.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume He: eps ∈ beta ∩ gamma.
Apply binintersectE beta gamma eps He to the current goal.
Assume He1 He2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ eps q r.
Assume Hqr4: ¬ q eps.
Assume Hqr5: r eps.
We prove the intermediate claim Le: ordinal eps.
An exact proof term for the current goal is ordinal_Hered beta Hb eps He1.
Apply ordinal_trichotomy_or alpha eps Ha Le to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: alpha ∈ eps.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ gamma.
An exact proof term for the current goal is Hc1 eps He2 alpha H1.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ alpha q r.
Apply PNoEq_antimon_ q r eps Le alpha H1 to the current goal.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove r alpha.
An exact proof term for the current goal is iffEL (q alpha) (r alpha) (Hqr3 alpha H1) Hpq3.
Assume H1: alpha = eps.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ gamma.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is He2.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ alpha q r.
rewrite the current goal using H1 (from left to right).
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove r alpha.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr5.
Assume H1: eps ∈ alpha.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p q r to the current goal.
We will prove PNoEq_ eps p q.
Apply PNoEq_antimon_ p q alpha Ha eps H1 to the current goal.
We will prove PNoEq_ alpha p q.
An exact proof term for the current goal is Hpq2.
We will prove PNoEq_ eps q r.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p eps.
Assume H2: p eps.
Apply Hqr4 to the current goal.
We will prove q eps.
An exact proof term for the current goal is iffEL (p eps) (q eps) (Hpq2 eps H1) H2.
We will prove r eps.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: beta ∈ gamma.
Assume Hqr2: PNoEq_ beta q r.
Assume Hqr3: r beta.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ gamma.
An exact proof term for the current goal is Hc1 beta Hqr1 alpha Hpq1.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
An exact proof term for the current goal is Hpq2.
Apply PNoEq_antimon_ q r beta Hb alpha Hpq1 to the current goal.
An exact proof term for the current goal is Hqr2.
We will prove r alpha.
An exact proof term for the current goal is iffEL (q alpha) (r alpha) (Hqr2 alpha Hpq1) Hpq3.
Assume Hqr1: gamma ∈ beta.
Assume Hqr2: PNoEq_ gamma q r.
Assume Hqr3: ¬ q gamma.
We will prove PNoLt alpha p gamma r.
Apply ordinal_trichotomy_or alpha gamma Ha Hc to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: alpha ∈ gamma.
Apply PNoLtI2 to the current goal.
We will prove alpha ∈ gamma.
An exact proof term for the current goal is H1.
We will prove PNoEq_ alpha p r.
Apply PNoEq_tra_ alpha p q r to the current goal.
An exact proof term for the current goal is Hpq2.
Apply PNoEq_antimon_ q r gamma Hc alpha H1 to the current goal.
An exact proof term for the current goal is Hqr2.
We will prove r alpha.
An exact proof term for the current goal is iffEL (q alpha) (r alpha) (Hqr2 alpha H1) Hpq3.
Assume H1: alpha = gamma.
We will prove False.
Apply Hqr3 to the current goal.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq3.
Assume H1: gamma ∈ alpha.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is H1.
We will prove PNoEq_ gamma p r.
Apply PNoEq_tra_ gamma p q r to the current goal.
Apply PNoEq_antimon_ p q alpha Ha gamma H1 to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p gamma.
Assume H2: p gamma.
Apply Hqr3 to the current goal.
We will prove q gamma.
An exact proof term for the current goal is iffEL (p gamma) (q gamma) (Hpq2 gamma H1) H2.
Assume Hpq1: beta ∈ alpha.
Assume Hpq2: PNoEq_ beta p q.
Assume Hpq3: ¬ p beta.
Apply PNoLtE beta gamma q r Hqr to the current goal.
Assume Hqr1: PNoLt_ (beta ∩ gamma) q r.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2.
Apply Hqr2 to the current goal.
Assume He: eps ∈ beta ∩ gamma.
Apply binintersectE beta gamma eps He to the current goal.
Assume He1 He2.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3.
Apply Hqr3 to the current goal.
Assume Hqr3: PNoEq_ eps q r.
Assume Hqr4: ¬ q eps.
Assume Hqr5: r eps.
We will prove PNoLt alpha p gamma r.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ gamma.
Apply binintersectI to the current goal.
We will prove eps ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hpq1 eps He1.
An exact proof term for the current goal is He2.
Apply and3I to the current goal.
We will prove PNoEq_ eps p r.
Apply PNoEq_tra_ eps p q r to the current goal.
We will prove PNoEq_ eps p q.
Apply PNoEq_antimon_ p q beta Hb eps He1 to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr3.
We will prove ¬ p eps.
Assume H1: p eps.
Apply Hqr4 to the current goal.
We will prove q eps.
An exact proof term for the current goal is iffEL (p eps) (q eps) (Hpq2 eps He1) H1.
We will prove r eps.
An exact proof term for the current goal is Hqr5.
Assume Hqr1: beta ∈ gamma.
Assume Hqr2: PNoEq_ beta q r.
Assume Hqr3: r beta.
Apply PNoLtI1 to the current goal.
We will prove ∃delta ∈ alpha ∩ gamma, PNoEq_ delta p r ∧ ¬ p delta ∧ r delta.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hpq1.
An exact proof term for the current goal is Hqr1.
Apply and3I to the current goal.
Apply PNoEq_tra_ beta p q r to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p beta.
An exact proof term for the current goal is Hpq3.
We will prove r beta.
An exact proof term for the current goal is Hqr3.
Assume Hqr1: gamma ∈ beta.
Assume Hqr2: PNoEq_ gamma q r.
Assume Hqr3: ¬ q gamma.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hpq1 gamma Hqr1.
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.
Apply PNoEq_antimon_ p q beta Hb gamma Hqr1 to the current goal.
An exact proof term for the current goal is Hpq2.
An exact proof term for the current goal is Hqr2.
We will prove ¬ p gamma.
Assume H1: p gamma.
Apply Hqr3 to the current goal.
We will prove q gamma.
An exact proof term for the current goal is iffEL (p gamma) (q gamma) (Hpq2 gamma Hqr1) H1.
∎