Let L and R be given.
Let alpha be given.
Assume Ha.
Apply Ha to the current goal.
Assume Ha1 _.
Assume HaL HaR.
Let p be given.
Assume Hp1: PNo_rel_strict_imv L R alpha p.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b.
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ alpha of type set → prop.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
We prove the intermediate claim Lpp0e: PNoEq_ alpha p p0.
An exact proof term for the current goal is PNo_extend0_eq alpha p.
We will prove PNo_rel_strict_upperbd L (ordsucc alpha) p0 ∧ PNo_rel_strict_lowerbd R (ordsucc alpha) p0.
Apply andI to the current goal.
We will prove PNo_rel_strict_upperbd L (ordsucc alpha) p0.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc alpha.
Let q be given.
Assume Hq: PNo_downc L gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa gamma Hc.
We will prove PNoLt gamma q (ordsucc alpha) p0.
Apply Hq to the current goal.
Let delta be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal delta.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: L delta r.
Assume Hqr: PNoLe gamma q delta r.
Apply PNoLeLt_tra gamma delta (ordsucc alpha) Lc Hd Lsa q r p0 Hqr to the current goal.
We will prove PNoLt delta r (ordsucc alpha) p0.
We prove the intermediate claim Lda: delta ∈ alpha.
An exact proof term for the current goal is HaL delta r Hr.
We prove the intermediate claim Ldsa: delta ∈ ordsucc alpha.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is Lda.
We prove the intermediate claim Ldr: PNo_downc L delta r.
An exact proof term for the current goal is PNo_downc_ref L delta Hd r Hr.
We prove the intermediate claim Lrp: PNoLt delta r alpha p.
An exact proof term for the current goal is Hp1a delta Lda r Ldr.
Apply PNoLt_trichotomy_or delta (ordsucc alpha) r p0 Hd Lsa to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1.
Apply H1 to the current goal.
Assume H2: delta = ordsucc alpha.
We will prove False.
Apply In_irref delta to the current goal.
rewrite the current goal using H2 (from left to right) at position 2.
An exact proof term for the current goal is Ldsa.
Assume H1: PNoLt (ordsucc alpha) p0 delta r.
We will prove False.
Apply PNoLt_irref delta r to the current goal.
Apply PNoLt_tra delta alpha delta Hd Ha Hd r p r Lrp to the current goal.
We will prove PNoLt alpha p delta r.
Apply PNoLtE (ordsucc alpha) delta p0 r H1 to the current goal.
Assume H2: PNoLt_ (ordsucc alpha ∩ delta) p0 r.
Apply H2 to the current goal.
Let eps be given.
Assume H3.
Apply H3 to the current goal.
Assume He: eps ∈ ordsucc alpha ∩ delta.
Apply binintersectE (ordsucc alpha) delta eps He to the current goal.
Assume He1 He2.
We prove the intermediate claim Lea: eps ∈ alpha.
An exact proof term for the current goal is Ha1 delta Lda eps He2.
Assume H3.
Apply H3 to the current goal.
Assume H3.
Apply H3 to the current goal.
Assume H3: PNoEq_ eps p0 r.
Assume H4: ¬ p0 eps.
Assume H5: r eps.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (alpha ∩ delta) p r.
We will prove ∃beta ∈ alpha ∩ delta, PNoEq_ beta p r ∧ ¬ p beta ∧ r beta.
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ delta.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Lea.
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 p0 r to the current goal.
Apply PNoEq_antimon_ p p0 alpha Ha eps Lea to the current goal.
An exact proof term for the current goal is Lpp0e.
An exact proof term for the current goal is H3.
We will prove ¬ p eps.
Assume H5: p eps.
Apply H4 to the current goal.
We will prove p eps ∧ eps ≠ alpha.
Apply andI to the current goal.
An exact proof term for the current goal is H5.
We will prove eps ≠ alpha.
Assume H6: eps = alpha.
Apply In_irref alpha to the current goal.
rewrite the current goal using H6 (from right to left) at position 1.
An exact proof term for the current goal is Lea.
We will prove r eps.
An exact proof term for the current goal is H5.
Assume H2: ordsucc alpha ∈ delta.
We will prove False.
An exact proof term for the current goal is In_no2cycle delta (ordsucc alpha) Ldsa H2.
Assume H2: delta ∈ ordsucc alpha.
Assume H3: PNoEq_ delta p0 r.
Assume H4: ¬ p0 delta.
Apply PNoLtI3 alpha delta p r Lda to the current goal.
We will prove PNoEq_ delta p r.
Apply PNoEq_tra_ delta p p0 r to the current goal.
Apply PNoEq_antimon_ p p0 alpha Ha delta Lda to the current goal.
An exact proof term for the current goal is Lpp0e.
An exact proof term for the current goal is H3.
We will prove ¬ p delta.
Assume H5: p delta.
Apply H4 to the current goal.
We will prove p delta ∧ delta ≠ alpha.
Apply andI to the current goal.
An exact proof term for the current goal is H5.
We will prove delta ≠ alpha.
Assume H6: delta = alpha.
Apply In_irref alpha to the current goal.
rewrite the current goal using H6 (from right to left) at position 1.
An exact proof term for the current goal is Lda.
We will prove PNo_rel_strict_lowerbd R (ordsucc alpha) p0.
Let gamma be given.
Assume Hc: gamma ∈ ordsucc alpha.
Let q be given.
Assume Hq: PNo_upc R gamma q.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa gamma Hc.
We will prove PNoLt (ordsucc alpha) p0 gamma q.
Apply PNoLt_tra (ordsucc alpha) alpha gamma Lsa Ha Lc p0 p q to the current goal.
We will prove PNoLt (ordsucc alpha) p0 alpha p.
Apply PNoLtI3 to the current goal.
We will prove alpha ∈ ordsucc alpha.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ alpha p0 p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lpp0e.
We will prove ¬ p0 alpha.
Assume H2: p0 alpha.
Apply H2 to the current goal.
Assume H3: p alpha.
Assume H4: alpha ≠ alpha.
Apply H4 to the current goal.
Use reflexivity.
We will prove PNoLt alpha p gamma q.
Apply Hq to the current goal.
Let delta be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hd: ordinal delta.
Assume Hq1.
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1.
Apply Hq1 to the current goal.
Assume Hr: R delta r.
Assume Hrq: PNoLe delta r gamma q.
We prove the intermediate claim Ldr: PNo_upc R delta r.
An exact proof term for the current goal is PNo_upc_ref R delta Hd r Hr.
Apply (λH : PNoLt alpha p delta r ⇒ PNoLtLe_tra alpha delta gamma Ha Hd Lc p r q H Hrq) to the current goal.
We will prove PNoLt alpha p delta r.
An exact proof term for the current goal is Hp1b delta (HaR delta r Hr) r Ldr.
∎