We will prove PNo_rel_strict_upperbd L (ordsucc α) p0.

Let γ be given.

Assume Hc: γ ∈ ordsucc α.

Let q be given.

Assume Hq: PNo_downc L γ q.

We prove the intermediate claim Lc: ordinal γ.

An exact proof term for the current goal is ordinal_Hered (ordsucc α) Lsa γ Hc.

We will prove PNoLt γ q (ordsucc α) p0.

Apply Hq to the current goal.

Let δ be given.

Assume Hq1.

Apply Hq1 to the current goal.

Assume Hd: ordinal δ.

Assume Hq1.

Apply Hq1 to the current goal.

Let r be given.

Assume Hq1.

Apply Hq1 to the current goal.

Assume Hr: L δ r.

Assume Hqr: PNoLe γ q δ r.

Apply PNoLeLt_tra γ δ (ordsucc α) Lc Hd Lsa q r p0 Hqr to the current goal.

We will prove PNoLt δ r (ordsucc α) p0.

We prove the intermediate claim Lda: δ ∈ α.

An exact proof term for the current goal is HaL δ r Hr.

We prove the intermediate claim Ldsa: δ ∈ ordsucc α.

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 δ r.

An exact proof term for the current goal is PNo_downc_ref L δ Hd r Hr.

We prove the intermediate claim Lrp: PNoLt δ r α p.

An exact proof term for the current goal is Hp1a δ Lda r Ldr.

Apply PNoLt_trichotomy_or δ (ordsucc α) 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: δ = ordsucc α.

We will prove False.

Apply In_irref δ 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 α) p0 δ r.

We will prove False.

Apply PNoLt_irref δ r to the current goal.

Apply PNoLt_tra δ α δ Hd Ha Hd r p r Lrp to the current goal.

We will prove PNoLt α p δ r.

Apply PNoLtE (ordsucc α) δ p0 r H1 to the current goal.

Assume H2: PNoLt_ (ordsucc α ∩ δ) p0 r.

Apply H2 to the current goal.

Let eps be given.

Assume H3.

Apply H3 to the current goal.

Assume He: eps ∈ ordsucc α ∩ δ.

Apply binintersectE (ordsucc α) δ eps He to the current goal.

Assume He1 He2.

We prove the intermediate claim Lea: eps ∈ α.

An exact proof term for the current goal is Ha1 δ 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_ (α ∩ δ) p r.

We will prove ∃β ∈ α ∩ δ, PNoEq_ β p r ∧ ¬ p β ∧ r β.

We use eps to witness the existential quantifier.

Apply andI to the current goal.

We will prove eps ∈ α ∩ δ.

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 α 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 ≠ α.

Apply andI to the current goal.

An exact proof term for the current goal is H5.

We will prove eps ≠ α.

Assume H6: eps = α.

Apply In_irref α 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 α ∈ δ.

We will prove False.

An exact proof term for the current goal is In_no2cycle δ (ordsucc α) Ldsa H2.

Assume H2: δ ∈ ordsucc α.

Assume H3: PNoEq_ δ p0 r.

Assume H4: ¬ p0 δ.

Apply PNoLtI3 α δ p r Lda to the current goal.

We will prove PNoEq_ δ p r.

Apply PNoEq_tra_ δ p p0 r to the current goal.

Apply PNoEq_antimon_ p p0 α Ha δ 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 δ.

Assume H5: p δ.

Apply H4 to the current goal.

We will prove p δ ∧ δ ≠ α.

Apply andI to the current goal.

An exact proof term for the current goal is H5.

We will prove δ ≠ α.

Assume H6: δ = α.

Apply In_irref α 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 α) p0.

Let γ be given.

Assume Hc: γ ∈ ordsucc α.

Let q be given.

Assume Hq: PNo_upc R γ q.

We prove the intermediate claim Lc: ordinal γ.

An exact proof term for the current goal is ordinal_Hered (ordsucc α) Lsa γ Hc.

We will prove PNoLt (ordsucc α) p0 γ q.

Apply PNoLt_tra (ordsucc α) α γ Lsa Ha Lc p0 p q to the current goal.

We will prove PNoLt (ordsucc α) p0 α p.

Apply PNoLtI3 to the current goal.

We will prove α ∈ ordsucc α.

Apply ordsuccI2 to the current goal.

We will prove PNoEq_ α p0 p.

Apply PNoEq_sym_ to the current goal.

An exact proof term for the current goal is Lpp0e.

We will prove ¬ p0 α.

Assume H2: p0 α.

Apply H2 to the current goal.

Assume H3: p α.

Assume H4: α ≠ α.

Apply H4 to the current goal.

Use reflexivity.

We will prove PNoLt α p γ q.

Apply Hq to the current goal.

Let δ be given.

Assume Hq1.

Apply Hq1 to the current goal.

Assume Hd: ordinal δ.

Assume Hq1.

Apply Hq1 to the current goal.

Let r be given.

Assume Hq1.

Apply Hq1 to the current goal.

Assume Hr: R δ r.

Assume Hrq: PNoLe δ r γ q.

We prove the intermediate claim Ldr: PNo_upc R δ r.

An exact proof term for the current goal is PNo_upc_ref R δ Hd r Hr.

Apply (λH : PNoLt α p δ r ⇒ PNoLtLe_tra α δ γ Ha Hd Lc p r q H Hrq) to the current goal.

We will prove PNoLt α p δ r.

An exact proof term for the current goal is Hp1b δ (HaR δ r Hr) r Ldr.