Let alpha and beta be given.

Assume Ha Hb.

Let p, q and r be given.

Assume Hpq.

Assume Hqr: PNoLt alpha q beta r ∨ alpha = beta ∧ PNoEq_ alpha q r.

We will prove PNoLt alpha p beta r ∨ alpha = beta ∧ PNoEq_ alpha p r.

Apply Hqr to the current goal.

Assume Hqr1.

Apply orIL to the current goal.

An exact proof term for the current goal is PNoEqLt_tra alpha beta Ha Hb p q r Hpq Hqr1.

Assume Hqr.

Apply Hqr to the current goal.

Assume Hqr1: alpha = beta.

Assume Hqr2: PNoEq_ alpha q r.

Apply orIR to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hqr1.

An exact proof term for the current goal is PNoEq_tra_ alpha p q r Hpq Hqr2.

∎