Let L and alpha be given.
Assume Ha: ordinal alpha.
Let beta be given.
Assume Hb: beta ∈ ordsucc alpha.
Let p be given.
Assume H1: PNo_strict_upperbd L alpha p.
Let gamma be given.
Assume Hc: gamma ∈ beta.
Let q be given.
Assume Hq: PNo_downc L gamma q.
Apply Ha to the current goal.
Assume Ha1 _.
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 Lb: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (ordsucc alpha) Lsa beta Hb.
We prove the intermediate claim Lb1: TransSet beta.
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 gamma.
An exact proof term for the current goal is ordinal_Hered beta Lb gamma Hc.
We prove the intermediate claim Lcb: gamma ⊆ beta.
An exact proof term for the current goal is Lb1 gamma Hc.
We will prove PNoLt gamma q beta p.
Apply Hq to the current goal.
Let delta be given.
Assume H2.
Apply H2 to the current goal.
Assume Hd: ordinal delta.
Assume H2.
Apply H2 to the current goal.
Let r be given.
Assume H2.
Apply H2 to the current goal.
Assume H2: L delta r.
Assume H3: PNoLe gamma q delta r.
We prove the intermediate claim L1: PNoLt delta r alpha p.
An exact proof term for the current goal is H1 delta Hd r H2.
We prove the intermediate claim L2: PNoLt gamma q alpha p.
An exact proof term for the current goal is PNoLeLt_tra gamma delta alpha Lc Hd Ha q r p H3 L1.
We prove the intermediate claim Lca: gamma ∈ alpha.
Apply ordsuccE alpha beta Hb to the current goal.
Assume Hb1: beta ∈ alpha.
An exact proof term for the current goal is Ha1 beta Hb1 gamma Hc.
Assume Hb1: beta = alpha.
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: gamma ⊆ alpha.
An exact proof term for the current goal is Ha1 gamma Lca.
We will prove PNoLt gamma q beta p.
Apply PNoLt_trichotomy_or gamma beta q p Lc Lb to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4.
An exact proof term for the current goal is H4.
Assume H4.
Apply H4 to the current goal.
Assume H4: gamma = beta.
We will prove False.
Apply In_irref beta 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: PNoLt beta p gamma q.
We will prove False.
Apply PNoLtE beta gamma p q H4 to the current goal.
rewrite the current goal using binintersect_com (from left to right).
rewrite the current goal using binintersect_Subq_eq_1 gamma beta Lcb (from left to right).
Assume H5: PNoLt_ gamma p q.
Apply H5 to the current goal.
Apply PNoLt_irref alpha p to the current goal.
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will prove PNoLt alpha p gamma q.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (alpha ∩ gamma) p q.
rewrite the current goal using binintersect_com (from left to right).
rewrite the current goal using binintersect_Subq_eq_1 gamma alpha Lca2 (from left to right).
We will prove PNoLt_ gamma p q.
An exact proof term for the current goal is H5.
We will prove PNoLt gamma q alpha p.
An exact proof term for the current goal is L2.
Assume H5: beta ∈ gamma.
We will prove False.
An exact proof term for the current goal is In_no2cycle beta gamma H5 Hc.
Assume H5: gamma ∈ beta.
Assume H6: PNoEq_ gamma p q.
Assume H7: ¬ p gamma.
Apply PNoLt_irref alpha p to the current goal.
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will prove PNoLt alpha p gamma q.
Apply PNoLtI3 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Lca.
We will prove PNoEq_ gamma p q.
An exact proof term for the current goal is H6.
We will prove ¬ p gamma.
An exact proof term for the current goal is H7.
We will prove PNoLt gamma q alpha p.
An exact proof term for the current goal is L2.
∎