Let α, p and q be given.

Assume H1.

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

Apply orIR to the current goal.

Apply andI to the current goal.

Use reflexivity.

An exact proof term for the current goal is H1.

∎