Let L and R be given.
Let alpha be given.
Assume Ha: ordinal alpha.
Let p be given.
Assume Hp: PNo_rel_strict_split_imv L R alpha p.
We prove the intermediate claim Lsa: ordinal (ordsucc alpha).
An exact proof term for the current goal is ordinal_ordsucc alpha Ha.
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ alpha of type set → prop.
Set p1 to be the term λdelta ⇒ p delta ∨ delta = alpha of type set → prop.
Apply Hp to the current goal.
Assume Hp0: PNo_rel_strict_imv L R (ordsucc alpha) p0.
Assume Hp1: PNo_rel_strict_imv L R (ordsucc alpha) p1.
Apply Hp0 to the current goal.
Assume Hp0a: PNo_rel_strict_upperbd L (ordsucc alpha) p0.
Assume Hp0b: PNo_rel_strict_lowerbd R (ordsucc alpha) p0.
Apply Hp1 to the current goal.
Assume Hp1a: PNo_rel_strict_upperbd L (ordsucc alpha) p1.
Assume Hp1b: PNo_rel_strict_lowerbd R (ordsucc alpha) p1.
We prove the intermediate claim Lnp0a: ¬ p0 alpha.
Assume H10.
Apply H10 to the current goal.
Assume H11: p alpha.
Assume H12: alpha ≠ alpha.
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lp1a: p1 alpha.
We will prove p alpha ∨ alpha = alpha.
Apply orIR to the current goal.
Use reflexivity.
We prove the intermediate claim Lap0p: PNoLt (ordsucc alpha) p0 alpha p.
Apply PNoLtI3 to the current goal.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ alpha p0 p.
Apply PNoEq_sym_ to the current goal.
Apply PNo_extend0_eq to the current goal.
We will prove ¬ p0 alpha.
An exact proof term for the current goal is Lnp0a.
We prove the intermediate claim Lapp1: PNoLt alpha p (ordsucc alpha) p1.
Apply PNoLtI2 to the current goal.
Apply ordsuccI2 to the current goal.
We will prove PNoEq_ alpha p p1.
Apply PNo_extend1_eq to the current goal.
We will prove p1 alpha.
An exact proof term for the current goal is Lp1a.
We will prove PNo_strict_upperbd L alpha p ∧ PNo_strict_lowerbd R alpha p.
Apply andI to the current goal.
Let beta be given.
Assume Hb: ordinal beta.
Let q be given.
Assume Hq: L beta q.
We will prove PNoLt beta q alpha p.
We prove the intermediate claim L4: PNo_downc L beta q.
Apply PNo_downc_ref L beta Hb to the current goal.
An exact proof term for the current goal is Hq.
We prove the intermediate claim L5: beta ∈ ordsucc alpha → PNoLt beta q alpha p.
Assume H10: beta ∈ ordsucc alpha.
Apply PNoLt_tra beta (ordsucc alpha) alpha Hb Lsa Ha q p0 p to the current goal.
We will prove PNoLt beta q (ordsucc alpha) p0.
Apply Hp0a beta H10 q to the current goal.
We will prove PNo_downc L beta q.
An exact proof term for the current goal is L4.
An exact proof term for the current goal is Lap0p.
We prove the intermediate claim L6: ∀gamma ∈ ordsucc alpha, gamma ∈ beta → PNoEq_ gamma p q → q gamma → p0 gamma.
Let gamma be given.
Assume Hc1: gamma ∈ ordsucc alpha.
Assume Hc2: gamma ∈ beta.
Assume H10: PNoEq_ gamma p q.
Assume H11: q gamma.
Apply dneg to the current goal.
Assume HNC: ¬ p0 gamma.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered beta Hb gamma Hc2.
We prove the intermediate claim L6a: PNoLt gamma q beta q.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is Hc2.
We will prove PNoEq_ gamma q q.
Apply PNoEq_ref_ to the current goal.
We will prove q gamma.
An exact proof term for the current goal is H11.
We prove the intermediate claim L6b: PNo_downc L gamma q.
We will prove ∃delta, ordinal delta ∧ ∃r : set → prop, L delta r ∧ PNoLe gamma q delta r.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
Apply PNoLeI1 to the current goal.
An exact proof term for the current goal is L6a.
We prove the intermediate claim L6c: PNoLt gamma q (ordsucc alpha) p0.
An exact proof term for the current goal is Hp0a gamma Hc1 q L6b.
We prove the intermediate claim L6d: PNoLt (ordsucc alpha) p0 gamma q.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is Hc1.
We will prove PNoEq_ gamma p0 q.
Apply PNoEq_tra_ gamma p0 p q to the current goal.
Apply PNoEq_sym_ to the current goal.
We will prove PNoEq_ gamma p p0.
Apply ordsuccE alpha gamma Hc1 to the current goal.
Assume H12: gamma ∈ alpha.
Apply PNoEq_antimon_ p p0 alpha Ha gamma H12 to the current goal.
We will prove PNoEq_ alpha p p0.
An exact proof term for the current goal is PNo_extend0_eq alpha p.
Assume H12: gamma = alpha.
rewrite the current goal using H12 (from left to right).
We will prove PNoEq_ alpha p p0.
An exact proof term for the current goal is PNo_extend0_eq alpha p.
An exact proof term for the current goal is H10.
We will prove ¬ p0 gamma.
An exact proof term for the current goal is HNC.
Apply PNoLt_irref gamma q to the current goal.
An exact proof term for the current goal is PNoLt_tra gamma (ordsucc alpha) gamma Lc Lsa Lc q p0 q L6c L6d.
Apply PNoLt_trichotomy_or alpha beta p q Ha Hb to the current goal.
Assume H10.
Apply H10 to the current goal.
Assume H10: PNoLt alpha p beta q.
Apply PNoLtE alpha beta p q H10 to the current goal.
Assume H11: PNoLt_ (alpha ∩ beta) p q.
Apply H11 to the current goal.
Let gamma be given.
Assume H12.
Apply H12 to the current goal.
Assume Hc: gamma ∈ alpha ∩ beta.
Assume H12.
Apply H12 to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoEq_ gamma p q.
Assume H13: ¬ p gamma.
Assume H14: q gamma.
We will prove False.
Apply binintersectE alpha beta gamma Hc to the current goal.
Assume Hc1: gamma ∈ alpha.
Assume Hc2: gamma ∈ beta.
Apply L6 gamma (ordsuccI1 alpha gamma Hc1) Hc2 H12 H14 to the current goal.
Assume H15: p gamma.
Assume _.
Apply H13 to the current goal.
An exact proof term for the current goal is H15.
Assume H11: alpha ∈ beta.
Assume H12: PNoEq_ alpha p q.
Assume H13: q alpha.
We will prove False.
Apply Lnp0a to the current goal.
We will prove p0 alpha.
An exact proof term for the current goal is L6 alpha (ordsuccI2 alpha) H11 H12 H13.
Assume H11: beta ∈ alpha.
Assume _ _.
Apply L5 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H11.
Assume H10.
Apply H10 to the current goal.
Assume H10a: alpha = beta.
Assume H10b: PNoEq_ alpha p q.
Apply L5 to the current goal.
We will prove beta ∈ ordsucc alpha.
rewrite the current goal using H10a (from right to left).
Apply ordsuccI2 to the current goal.
Assume H10: PNoLt beta q alpha p.
An exact proof term for the current goal is H10.
Let beta be given.
Assume Hb: ordinal beta.
Let q be given.
Assume Hq: R beta q.
We will prove PNoLt alpha p beta q.
We prove the intermediate claim L4: PNo_upc R beta q.
Apply PNo_upc_ref R beta Hb to the current goal.
An exact proof term for the current goal is Hq.
We prove the intermediate claim L5: beta ∈ ordsucc alpha → PNoLt alpha p beta q.
Assume H10: beta ∈ ordsucc alpha.
Apply PNoLt_tra alpha (ordsucc alpha) beta Ha Lsa Hb p p1 q to the current goal.
An exact proof term for the current goal is Lapp1.
We will prove PNoLt (ordsucc alpha) p1 beta q.
Apply Hp1b beta H10 q to the current goal.
We will prove PNo_upc R beta q.
An exact proof term for the current goal is L4.
We prove the intermediate claim L6: ∀gamma ∈ ordsucc alpha, gamma ∈ beta → PNoEq_ gamma q p → p1 gamma → q gamma.
Let gamma be given.
Assume Hc1: gamma ∈ ordsucc alpha.
Assume Hc2: gamma ∈ beta.
Assume H10: PNoEq_ gamma q p.
Assume H11: p1 gamma.
Apply dneg to the current goal.
Assume HNC: ¬ q gamma.
We prove the intermediate claim Lc: ordinal gamma.
An exact proof term for the current goal is ordinal_Hered beta Hb gamma Hc2.
We prove the intermediate claim L6a: PNoLt beta q gamma q.
Apply PNoLtI3 to the current goal.
An exact proof term for the current goal is Hc2.
We will prove PNoEq_ gamma q q.
Apply PNoEq_ref_ to the current goal.
We will prove ¬ q gamma.
An exact proof term for the current goal is HNC.
We prove the intermediate claim L6b: PNo_upc R gamma q.
We will prove ∃delta, ordinal delta ∧ ∃r : set → prop, R delta r ∧ PNoLe delta r gamma q.
We use beta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb.
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq.
Apply PNoLeI1 to the current goal.
An exact proof term for the current goal is L6a.
We prove the intermediate claim L6c: PNoLt (ordsucc alpha) p1 gamma q.
An exact proof term for the current goal is Hp1b gamma Hc1 q L6b.
We prove the intermediate claim L6d: PNoLt gamma q (ordsucc alpha) p1.
Apply PNoLtI2 to the current goal.
An exact proof term for the current goal is Hc1.
We will prove PNoEq_ gamma q p1.
Apply PNoEq_tra_ gamma q p p1 to the current goal.
An exact proof term for the current goal is H10.
We will prove PNoEq_ gamma p p1.
Apply ordsuccE alpha gamma Hc1 to the current goal.
Assume H12: gamma ∈ alpha.
Apply PNoEq_antimon_ p p1 alpha Ha gamma H12 to the current goal.
We will prove PNoEq_ alpha p p1.
An exact proof term for the current goal is PNo_extend1_eq alpha p.
Assume H12: gamma = alpha.
rewrite the current goal using H12 (from left to right).
We will prove PNoEq_ alpha p p1.
An exact proof term for the current goal is PNo_extend1_eq alpha p.
We will prove p1 gamma.
An exact proof term for the current goal is H11.
Apply PNoLt_irref gamma q to the current goal.
An exact proof term for the current goal is PNoLt_tra gamma (ordsucc alpha) gamma Lc Lsa Lc q p1 q L6d L6c.
Apply PNoLt_trichotomy_or alpha beta p q Ha Hb to the current goal.
Assume H10.
Apply H10 to the current goal.
Assume H10.
An exact proof term for the current goal is H10.
Assume H10.
Apply H10 to the current goal.
Assume H10a: alpha = beta.
Assume H10b: PNoEq_ alpha p q.
Apply L5 to the current goal.
We will prove beta ∈ ordsucc alpha.
rewrite the current goal using H10a (from right to left).
Apply ordsuccI2 to the current goal.
Assume H10: PNoLt beta q alpha p.
Apply PNoLtE beta alpha q p H10 to the current goal.
Assume H11: PNoLt_ (beta ∩ alpha) q p.
Apply H11 to the current goal.
Let gamma be given.
Assume H12.
Apply H12 to the current goal.
Assume Hc: gamma ∈ beta ∩ alpha.
Assume H12.
Apply H12 to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoEq_ gamma q p.
Assume H13: ¬ q gamma.
Assume H14: p gamma.
We will prove False.
Apply binintersectE beta alpha gamma Hc to the current goal.
Assume Hc2: gamma ∈ beta.
Assume Hc1: gamma ∈ alpha.
Apply H13 to the current goal.
Apply L6 gamma (ordsuccI1 alpha gamma Hc1) Hc2 H12 to the current goal.
We will prove p1 gamma.
We will prove p gamma ∨ gamma = alpha.
Apply orIL to the current goal.
An exact proof term for the current goal is H14.
Assume H11: beta ∈ alpha.
Assume _ _.
Apply L5 to the current goal.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H11.
Assume H11: alpha ∈ beta.
Assume H12: PNoEq_ alpha q p.
Assume H13: ¬ q alpha.
We will prove False.
Apply H13 to the current goal.
An exact proof term for the current goal is L6 alpha (ordsuccI2 alpha) H11 H12 Lp1a.
∎