Let R and α be given.
Assume Ha: ordinal α.
Let β be given.
Assume Hb: β ∈ ordsucc α.
Let p be given.
Assume H1: PNo_strict_lowerbd R α p.
Let γ be given.
Assume Hc: γ ∈ β.
Let q be given.
Assume Hq: PNo_upc R γ q.
Apply Ha to the current goal.
Assume Ha1 _.
We prove the intermediate claim Lsa: ordinal (ordsucc α).
An exact proof term for the current goal is ordinal_ordsucc α Ha.
We prove the intermediate claim Lb: ordinal β.
An exact proof term for the current goal is ordinal_Hered (ordsucc α) Lsa β Hb.
We prove the intermediate claim Lb1: TransSet β.
Apply Lb to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim Lc: ordinal γ.
An exact proof term for the current goal is ordinal_Hered β Lb γ Hc.
We prove the intermediate claim Lcb: γ ⊆ β.
An exact proof term for the current goal is Lb1 γ Hc.
We will prove PNoLt β p γ q.
Apply Hq to the current goal.
Let δ be given.
Assume H2.
Apply H2 to the current goal.
Assume Hd: ordinal δ.
Assume H2.
Apply H2 to the current goal.
Let r be given.
Assume H2.
Apply H2 to the current goal.
Assume H2: R δ r.
Assume H3: PNoLe δ r γ q.
We prove the intermediate claim L1: PNoLt α p δ r.
An exact proof term for the current goal is H1 δ Hd r H2.
We prove the intermediate claim L2: PNoLt α p γ q.
An exact proof term for the current goal is PNoLtLe_tra α δ γ Ha Hd Lc p r q L1 H3.
We prove the intermediate claim Lca: γ ∈ α.
Apply ordsuccE α β Hb to the current goal.
Assume Hb1: β ∈ α.
An exact proof term for the current goal is Ha1 β Hb1 γ Hc.
Assume Hb1: β = α.
rewrite the current goal using Hb1 (from right to left).
An exact proof term for the current goal is Hc.
We prove the intermediate claim Lca2: γ ⊆ α.
An exact proof term for the current goal is Ha1 γ Lca.
We will prove PNoLt β p γ q.
Apply PNoLt_trichotomy_or γ β q p Lc Lb to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4: PNoLt γ q β p.
We will prove False.
Apply PNoLtE γ β q p H4 to the current goal.
rewrite the current goal using binintersect_Subq_eq_1 γ β Lcb (from left to right).
Assume H5: PNoLt_ γ q p.
Apply H5 to the current goal.
Apply PNoLt_irref α p to the current goal.
Apply PNoLt_tra α γ α Ha Lc Ha p q p to the current goal.
We will prove PNoLt α p γ q.
An exact proof term for the current goal is L2.
We will prove PNoLt γ q α p.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (γ ∩ α) q p.
rewrite the current goal using binintersect_Subq_eq_1 γ α Lca2 (from left to right).
We will prove PNoLt_ γ q p.
An exact proof term for the current goal is H5.
Assume H5: γ ∈ β.
Assume H6: PNoEq_ γ q p.
Assume H7: p γ.
Apply PNoLt_irref α p to the current goal.
Apply PNoLt_tra α γ α Ha Lc Ha p q p to the current goal.
We will prove PNoLt α p γ q.
An exact proof term for the current goal is L2.
We will prove PNoLt γ q α p.
Apply PNoLtI2 to the current goal.
We will prove γ ∈ α.
An exact proof term for the current goal is Lca.
We will prove PNoEq_ γ q p.
An exact proof term for the current goal is H6.
We will prove p γ.
An exact proof term for the current goal is H7.
Assume H5: β ∈ γ.
We will prove False.
An exact proof term for the current goal is In_no2cycle β γ H5 Hc.
Assume H4.
Apply H4 to the current goal.
Assume H4: γ = β.
We will prove False.
Apply In_irref β to the current goal.
rewrite the current goal using H4 (from right to left) at position 1.
An exact proof term for the current goal is Hc.
Assume H4.
An exact proof term for the current goal is H4.
∎