Let a1, a2, b1 and b2 be given.

Assume Hrel: order_rel (setprod R R) (a1,a2) (b1,b2).

Apply (order_rel_setprod_R_R_unfold (a1,a2) (b1,b2) Hrel) to the current goal.

Let c1 be given.

Assume Hc1rest.

Apply Hc1rest to the current goal.

Let c2 be given.

Assume Hc2rest.

Apply Hc2rest to the current goal.

Let d1 be given.

Assume Hd1rest.

Apply Hd1rest to the current goal.

Let d2 be given.

Assume Hpack: ((a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2)) ∧ (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)).

We prove the intermediate claim Heqs: (a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2).

An exact proof term for the current goal is (andEL ((a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpack).

We prove the intermediate claim Hdisj: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).

An exact proof term for the current goal is (andER ((a1,a2) = (c1,c2) ∧ (b1,b2) = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpack).

We prove the intermediate claim HacEq: (a1,a2) = (c1,c2).

An exact proof term for the current goal is (andEL ((a1,a2) = (c1,c2)) ((b1,b2) = (d1,d2)) Heqs).

We prove the intermediate claim HbdEq: (b1,b2) = (d1,d2).

An exact proof term for the current goal is (andER ((a1,a2) = (c1,c2)) ((b1,b2) = (d1,d2)) Heqs).

We prove the intermediate claim Hacoords: a1 = c1 ∧ a2 = c2.

An exact proof term for the current goal is (tuple_eq_coords a1 a2 c1 c2 HacEq).

We prove the intermediate claim Hbcoords: b1 = d1 ∧ b2 = d2.

An exact proof term for the current goal is (tuple_eq_coords b1 b2 d1 d2 HbdEq).

We prove the intermediate claim Ha1eq: a1 = c1.

An exact proof term for the current goal is (andEL (a1 = c1) (a2 = c2) Hacoords).

We prove the intermediate claim Ha2eq: a2 = c2.

An exact proof term for the current goal is (andER (a1 = c1) (a2 = c2) Hacoords).

We prove the intermediate claim Hb1eq: b1 = d1.

An exact proof term for the current goal is (andEL (b1 = d1) (b2 = d2) Hbcoords).

We prove the intermediate claim Hb2eq: b2 = d2.

An exact proof term for the current goal is (andER (b1 = d1) (b2 = d2) Hbcoords).

Apply Hdisj to the current goal.

Assume Hc1ltd1: Rlt c1 d1.

Apply orIL to the current goal.

We will prove Rlt a1 b1.

rewrite the current goal using Ha1eq (from left to right) at position 1.

rewrite the current goal using Hb1eq (from left to right) at position 1.

An exact proof term for the current goal is Hc1ltd1.

Assume Hc1eqAnd: c1 = d1 ∧ Rlt c2 d2.

Apply Hc1eqAnd to the current goal.

Assume Hc1eqd1 Hc2ltd2.

Apply orIR to the current goal.

We will prove a1 = b1 ∧ Rlt a2 b2.

Apply andI to the current goal.

We will prove a1 = b1.

rewrite the current goal using Ha1eq (from left to right) at position 1.

rewrite the current goal using Hb1eq (from left to right) at position 1.

An exact proof term for the current goal is Hc1eqd1.

We will prove Rlt a2 b2.

rewrite the current goal using Ha2eq (from left to right) at position 1.

rewrite the current goal using Hb2eq (from left to right) at position 1.

An exact proof term for the current goal is Hc2ltd2.

∎