Let α, β, p and q be given.

Assume H1.

We will prove PNoLt α p β q ∨ α = β ∧ PNoEq_ α p q.

Apply orIL to the current goal.

An exact proof term for the current goal is H1.

∎