Let L and R be given.
Assume HLR.
We will prove PNoLt_pwise (PNo_downc L) (PNo_upc R).
Let gamma be given.
Assume Hc.
Let p be given.
Assume Hp.
Let delta be given.
Assume Hd.
Let q be given.
Assume Hq.
Apply Hp to the current goal.
Let alpha be given.
Assume H1.
Apply H1 to the current goal.
Assume H2: ordinal alpha.
Assume H3.
Apply H3 to the current goal.
Let p2 be given.
Assume H3.
Apply H3 to the current goal.
Assume H4: L alpha p2.
Assume H5: PNoLe gamma p alpha p2.
Apply Hq to the current goal.
Let beta be given.
Assume H6.
Apply H6 to the current goal.
Assume H7: ordinal beta.
Assume H8.
Apply H8 to the current goal.
Let q2 be given.
Assume H9.
Apply H9 to the current goal.
Assume H10: R beta q2.
Assume H11: PNoLe beta q2 delta q.
We prove the intermediate claim L1: PNoLt gamma p delta q.
Apply PNoLeLt_tra gamma alpha delta Hc H2 Hd p p2 q H5 to the current goal.
We will prove PNoLt alpha p2 delta q.
Apply PNoLtLe_tra alpha beta delta H2 H7 Hd p2 q2 q (HLR alpha H2 p2 H4 beta H7 q2 H10) to the current goal.
We will prove PNoLe beta q2 delta q.
An exact proof term for the current goal is H11.
Apply PNoLt_trichotomy_or delta gamma q p Hd Hc to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H12: PNoLt delta q gamma p.
Apply PNoLt_irref gamma p to the current goal.
We will prove PNoLt gamma p gamma p.
Apply PNoLt_tra gamma delta gamma Hc Hd Hc p q p L1 to the current goal.
An exact proof term for the current goal is H12.
Assume H12: delta = gamma ∧ PNoEq_ delta q p.
Apply PNoLt_irref delta q to the current goal.
We will prove PNoLt delta q delta q.
Apply PNoLeLt_tra delta gamma delta Hd Hc Hd q p q to the current goal.
We will prove PNoLe delta q gamma p.
We will prove PNoLt delta q gamma p ∨ delta = gamma ∧ PNoEq_ delta q p.
Apply orIR to the current goal.
An exact proof term for the current goal is H12.
We will prove PNoLt gamma p delta q.
An exact proof term for the current goal is L1.
Assume H12: PNoLt gamma p delta q.
An exact proof term for the current goal is H12.
∎