Let L and R be given.

Assume HLR.

We will prove PNoLt_pwise (PNo_downc L) (PNo_upc R).

Let γ be given.

Assume Hc.

Let p be given.

Assume Hp.

Let δ be given.

Assume Hd.

Let q be given.

Assume Hq.

Apply Hp to the current goal.

Let α be given.

Assume H1.

Apply H1 to the current goal.

Assume H2: ordinal α.

Assume H3.

Apply H3 to the current goal.

Let p2 be given.

Assume H3.

Apply H3 to the current goal.

Assume H4: L α p2.

Assume H5: PNoLe γ p α p2.

Apply Hq to the current goal.

Let β be given.

Assume H6.

Apply H6 to the current goal.

Assume H7: ordinal β.

Assume H8.

Apply H8 to the current goal.

Let q2 be given.

Assume H9.

Apply H9 to the current goal.

Assume H10: R β q2.

Assume H11: PNoLe β q2 δ q.

We prove the intermediate claim L1: PNoLt γ p δ q.

Apply PNoLeLt_tra γ α δ Hc H2 Hd p p2 q H5 to the current goal.

We will prove PNoLt α p2 δ q.

Apply PNoLtLe_tra α β δ H2 H7 Hd p2 q2 q (HLR α H2 p2 H4 β H7 q2 H10) to the current goal.

We will prove PNoLe β q2 δ q.

An exact proof term for the current goal is H11.

Apply PNoLt_trichotomy_or δ γ q p Hd Hc to the current goal.

Assume H12.

Apply H12 to the current goal.

Assume H12: PNoLt δ q γ p.

Apply PNoLt_irref γ p to the current goal.

We will prove PNoLt γ p γ p.

Apply PNoLt_tra γ δ γ Hc Hd Hc p q p L1 to the current goal.

An exact proof term for the current goal is H12.

Assume H12: δ = γ ∧ PNoEq_ δ q p.

Apply PNoLt_irref δ q to the current goal.

We will prove PNoLt δ q δ q.

Apply PNoLeLt_tra δ γ δ Hd Hc Hd q p q to the current goal.

We will prove PNoLe δ q γ p.

We will prove PNoLt δ q γ p ∨ δ = γ ∧ PNoEq_ δ q p.

Apply orIR to the current goal.

An exact proof term for the current goal is H12.

We will prove PNoLt γ p δ q.

An exact proof term for the current goal is L1.

Assume H12: PNoLt γ p δ q.

An exact proof term for the current goal is H12.

∎