Let α and β be given.
Assume Ha Hb.
Let p, q and r be given.
Assume Hpq.
Assume Hqr: PNoLt α q β r ∨ α = β ∧ PNoEq_ α q r.
We will prove PNoLt α p β r ∨ α = β ∧ PNoEq_ α 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 α β Ha Hb p q r Hpq Hqr1.
Assume Hqr.
Apply Hqr to the current goal.
Assume Hqr1: α = β.
Assume Hqr2: PNoEq_ α 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_ α p q r Hpq Hqr2.
∎