Assume H1: PNoLt α p β q.

We will prove False.

Apply H2 to the current goal.

Assume H2: PNoLt β q α p.

Apply PNoLt_irref α p to the current goal.

Apply PNoLt_tra α β α Ha Hb Ha p q p to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is H2.

Assume H2.

Apply H2 to the current goal.

Assume H2a: β = α.

Assume H2b: PNoEq_ β q p.

Apply PNoLtE α β p q H1 to the current goal.

Assume Hpq1: PNoLt_ (α ∩ β) p q.

Apply Hpq1 to the current goal.

Let δ be given.

Assume Hpq2.

Apply Hpq2 to the current goal.

Assume Hd: δ ∈ α ∩ β.

Apply binintersectE α β δ Hd to the current goal.

Assume Hd1 Hd2.

Assume Hpq3.

Apply Hpq3 to the current goal.

Assume Hpq3.

Apply Hpq3 to the current goal.

Assume Hpq3: PNoEq_ δ p q.

Assume Hpq4: ¬ p δ.

Assume Hpq5: q δ.

Apply Hpq4 to the current goal.

An exact proof term for the current goal is iffEL (q δ) (p δ) (H2b δ Hd2) Hpq5.

Assume Hpq1: α ∈ β.

Assume Hpq2: PNoEq_ α p q.

Assume Hpq3: q α.

Apply In_irref α to the current goal.

rewrite the current goal using H2a (from right to left) at position 2.

An exact proof term for the current goal is Hpq1.

Assume Hpq1: β ∈ α.

Assume Hpq2: PNoEq_ β p q.

Assume Hpq3: ¬ p β.

Apply In_irref α to the current goal.

rewrite the current goal using H2a (from right to left) at position 1.

An exact proof term for the current goal is Hpq1.