Let R 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_lowerbd R alpha p.
Let gamma be given.
Assume Hc: gamma ∈ beta.
Let q be given.
Assume Hq: PNo_upc R 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 beta p gamma q.
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: R delta r.
Assume H3: PNoLe delta r gamma q.
We prove the intermediate claim L1: PNoLt alpha p delta r.
An exact proof term for the current goal is H1 delta Hd r H2.
We prove the intermediate claim L2: PNoLt alpha p gamma q.
An exact proof term for the current goal is PNoLtLe_tra alpha delta gamma Ha Hd Lc p r q L1 H3.
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 beta p gamma q.
Apply PNoLt_trichotomy_or gamma beta q p Lc Lb to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4: PNoLt gamma q beta p.
We will prove False.
Apply PNoLtE gamma beta q p H4 to the current goal.
rewrite the current goal using binintersect_Subq_eq_1 gamma beta Lcb (from left to right).
Assume H5: PNoLt_ gamma q p.
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.
An exact proof term for the current goal is L2.
We will prove PNoLt gamma q alpha p.
Apply PNoLtI1 to the current goal.
We will prove PNoLt_ (gamma ∩ alpha) q p.
rewrite the current goal using binintersect_Subq_eq_1 gamma alpha Lca2 (from left to right).
We will prove PNoLt_ gamma q p.
An exact proof term for the current goal is H5.
Assume H5: gamma ∈ beta.
Assume H6: PNoEq_ gamma q p.
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.
An exact proof term for the current goal is L2.
We will prove PNoLt gamma q alpha p.
Apply PNoLtI2 to the current goal.
We will prove gamma ∈ alpha.
An exact proof term for the current goal is Lca.
We will prove PNoEq_ gamma q p.
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.
Assume H5: beta ∈ gamma.
We will prove False.
An exact proof term for the current goal is In_no2cycle beta gamma H5 Hc.
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.
An exact proof term for the current goal is H4.
∎