Let x, a2 and b2 be given.

Assume Hab: Rlt a2 b2.

Apply (order_rel_setprod_R_R_intro x a2 x b2) to the current goal.

Apply orIR to the current goal.

An exact proof term for the current goal is (andI (x = x) (Rlt a2 b2) (λP H ⇒ H) Hab).

∎