Let L and R be given.
Assume HLR.
Let alpha be given.
Assume Ha.
Let p and q be given.
Assume Hp.
Assume Hq.
Apply Ha to the current goal.
Assume Ha1 _.
Apply Hp to the current goal.
Assume Hp1.
Apply Hp1 to the current goal.
Assume _.
Assume Hp1: PNo_strict_imv L R alpha p.
Assume Hp2: ∀beta ∈ alpha, ∀r : set → prop, ¬ PNo_strict_imv L R beta r.
Apply Hp1 to the current goal.
Assume Hp1a: PNo_strict_upperbd L alpha p.
Assume Hp1b: PNo_strict_lowerbd R alpha p.
Apply Hq to the current goal.
Assume Hq1: PNo_strict_upperbd L alpha q.
Assume Hq2: PNo_strict_lowerbd R alpha q.
We prove the intermediate claim L1: ∀beta, ordinal beta → beta ∈ alpha → (p beta ↔ q beta).
Apply ordinal_ind to the current goal.
Let beta be given.
Assume Hb1: ordinal beta.
Assume IH: ∀gamma ∈ beta, gamma ∈ alpha → (p gamma ↔ q gamma).
Assume Hb2: beta ∈ alpha.
We prove the intermediate claim Lbpq: PNoEq_ beta p q.
Let gamma be given.
Assume Hc: gamma ∈ beta.
An exact proof term for the current goal is IH gamma Hc (Ha1 beta Hb2 gamma Hc).
We will prove p beta ↔ q beta.
Apply iffI to the current goal.
Assume H1: p beta.
We will prove q beta.
Apply dneg to the current goal.
Assume H2: ¬ q beta.
We prove the intermediate claim Lqp: PNoLt beta q alpha p.
Apply PNoLtI2 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ beta q p.
Apply PNoEq_sym_ to the current goal.
An exact proof term for the current goal is Lbpq.
We will prove p beta.
An exact proof term for the current goal is H1.
We prove the intermediate claim Lqq: PNoLt alpha q beta q.
Apply PNoLtI3 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ beta q q.
Apply PNoEq_ref_ to the current goal.
We will prove ¬ q beta.
An exact proof term for the current goal is H2.
Apply Hp2 beta Hb2 q to the current goal.
We will prove PNo_strict_imv L R beta q.
We will prove PNo_strict_upperbd L beta q ∧ PNo_strict_lowerbd R beta q.
Apply andI to the current goal.
Let gamma be given.
Assume Hc: ordinal gamma.
Let r be given.
Assume Hr: L gamma r.
We will prove PNoLt gamma r beta q.
Apply PNoLt_tra gamma alpha beta Hc Ha Hb1 r q q to the current goal.
We will prove PNoLt gamma r alpha q.
An exact proof term for the current goal is Hq1 gamma Hc r Hr.
We will prove PNoLt alpha q beta q.
An exact proof term for the current goal is Lqq.
Let gamma be given.
Assume Hc: ordinal gamma.
Let r be given.
Assume Hr: R gamma r.
We will prove PNoLt beta q gamma r.
Apply PNoLt_tra beta alpha gamma Hb1 Ha Hc q p r to the current goal.
We will prove PNoLt beta q alpha p.
An exact proof term for the current goal is Lqp.
We will prove PNoLt alpha p gamma r.
An exact proof term for the current goal is Hp1b gamma Hc r Hr.
Assume H1: q beta.
We will prove p beta.
Apply dneg to the current goal.
Assume H2: ¬ p beta.
We prove the intermediate claim Lpq: PNoLt alpha p beta q.
Apply PNoLtI3 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ beta p q.
An exact proof term for the current goal is Lbpq.
We will prove ¬ p beta.
An exact proof term for the current goal is H2.
We prove the intermediate claim Lqq: PNoLt beta q alpha q.
Apply PNoLtI2 to the current goal.
We will prove beta ∈ alpha.
An exact proof term for the current goal is Hb2.
We will prove PNoEq_ beta q q.
Apply PNoEq_ref_ to the current goal.
We will prove q beta.
An exact proof term for the current goal is H1.
Apply Hp2 beta Hb2 q to the current goal.
We will prove PNo_strict_imv L R beta q.
We will prove PNo_strict_upperbd L beta q ∧ PNo_strict_lowerbd R beta q.
Apply andI to the current goal.
Let gamma be given.
Assume Hc: ordinal gamma.
Let r be given.
Assume Hr: L gamma r.
We will prove PNoLt gamma r beta q.
Apply PNoLt_tra gamma alpha beta Hc Ha Hb1 r p q to the current goal.
We will prove PNoLt gamma r alpha p.
An exact proof term for the current goal is Hp1a gamma Hc r Hr.
We will prove PNoLt alpha p beta q.
An exact proof term for the current goal is Lpq.
Let gamma be given.
Assume Hc: ordinal gamma.
Let r be given.
Assume Hr: R gamma r.
We will prove PNoLt beta q gamma r.
Apply PNoLt_tra beta alpha gamma Hb1 Ha Hc q q r to the current goal.
We will prove PNoLt beta q alpha q.
An exact proof term for the current goal is Lqq.
We will prove PNoLt alpha q gamma r.
An exact proof term for the current goal is Hq2 gamma Hc r Hr.
Let beta be given.
Assume Hb: beta ∈ alpha.
An exact proof term for the current goal is L1 beta (ordinal_Hered alpha Ha beta Hb) Hb.
∎