Assume H1: PNoLt alpha p beta q.

We will prove False.

Apply H2 to the current goal.

Assume H2: PNoLt beta q alpha p.

Apply PNoLt_irref alpha p to the current goal.

Apply PNoLt_tra alpha beta alpha 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: beta = alpha.

Assume H2b: PNoEq_ beta q p.

Apply PNoLtE alpha beta p q H1 to the current goal.

Assume Hpq1: PNoLt_ (alpha ∩ beta) p q.

Apply Hpq1 to the current goal.

Let delta be given.

Assume Hpq2.

Apply Hpq2 to the current goal.

Assume Hd: delta ∈ alpha ∩ beta.

Apply binintersectE alpha beta delta 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_ delta p q.

Assume Hpq4: ¬ p delta.

Assume Hpq5: q delta.

Apply Hpq4 to the current goal.

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

Assume Hpq1: alpha ∈ beta.

Assume Hpq2: PNoEq_ alpha p q.

Assume Hpq3: q alpha.

Apply In_irref alpha 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: beta ∈ alpha.

Assume Hpq2: PNoEq_ beta p q.

Assume Hpq3: ¬ p beta.

Apply In_irref alpha 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.