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.

Assume H2: PNoLt beta q gamma r ∨ beta = gamma ∧ PNoEq_ beta q r.

Apply H2 to the current goal.

Assume H2: PNoLt beta q gamma r.

An exact proof term for the current goal is PNoLt_tra alpha beta gamma Ha Hb Hc p q r H1 H2.

Assume H2.

Apply H2 to the current goal.

Assume H2a: beta = gamma.

Assume H2b: PNoEq_ beta q r.

We will prove PNoLt alpha p gamma r.

rewrite the current goal using H2a (from right to left).

We will prove PNoLt alpha p beta r.

An exact proof term for the current goal is PNoLtEq_tra alpha beta Ha Hb p q r H1 H2b.

∎