Let α, β and γ be given.
Assume Ha Hb Hc.
Let p, q and r be given.
Assume H1: PNoLt α p β q.
Assume H2: PNoLt β q γ r ∨ β = γ ∧ PNoEq_ β q r.
Apply H2 to the current goal.
Assume H2: PNoLt β q γ r.
An exact proof term for the current goal is PNoLt_tra α β γ Ha Hb Hc p q r H1 H2.
Assume H2.
Apply H2 to the current goal.
Assume H2a: β = γ.
Assume H2b: PNoEq_ β q r.
We will prove PNoLt α p γ r.
rewrite the current goal using H2a (from right to left).
We will prove PNoLt α p β r.
An exact proof term for the current goal is PNoLtEq_tra α β Ha Hb p q r H1 H2b.
∎