Let a and b be given.

Assume Ha Hb Hnlt.

We will prove a ∈ R ∧ b ∈ R ∧ ¬ (Rlt b a).

Apply and3I to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is Hb.

An exact proof term for the current goal is Hnlt.

∎