Let α, β and γ be given.
Assume Ha Hb Hc.
Let p, q and r be given.
Assume H1: PNoLt α p β q ∨ α = β ∧ PNoEq_ α p q.
Assume H2: PNoLe β q γ r.
Apply H1 to the current goal.
Assume H1: PNoLt α p β q.
We will prove PNoLt α p γ r ∨ α = γ ∧ PNoEq_ α p r.
Apply orIL to the current goal.
An exact proof term for the current goal is PNoLtLe_tra α β γ Ha Hb Hc p q r H1 H2.
Assume H1.
Apply H1 to the current goal.
Assume H1a: α = β.
Assume H1b: PNoEq_ α p q.
We will prove PNoLe α p γ r.
rewrite the current goal using H1a (from left to right).
We will prove PNoLe β p γ r.
We prove the intermediate claim L1: PNoEq_ β p q.
rewrite the current goal using H1a (from right to left).
An exact proof term for the current goal is H1b.
An exact proof term for the current goal is PNoEqLe_tra β γ Hb Hc p q r L1 H2.
∎