Let alpha, beta and gamma be given.
Assume Ha Hb Hc.
Let p, q and r be given.
Assume H1: PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q.
Assume H2: PNoLt beta q gamma r.
Apply H1 to the current goal.
Assume H1: PNoLt alpha p beta q.
An exact proof term for the current goal is PNoLt_tra alpha beta gamma Ha Hb Hc p q r H1 H2.
Assume H1.
Apply H1 to the current goal.
Assume H1a: alpha = beta.
Assume H1b: PNoEq_ alpha p q.
We will prove PNoLt alpha p gamma r.
rewrite the current goal using H1a (from left to right).
We will prove PNoLt beta p gamma r.
Apply PNoEqLt_tra beta gamma Hb Hc p q r to the current goal.
We will prove PNoEq_ beta 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 H2.
∎