Let a and b be given.
Assume Hrel: order_rel (setprod R R) a b.
Apply (Hrel (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)))) to the current goal.
Assume Hleft6.
Apply (Hleft6 (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)))) to the current goal.
Assume Hleft.
Apply (Hleft (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)))) to the current goal.
Assume Hmid.
Apply (Hmid (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)))) to the current goal.
Assume Hm2.
Apply (Hm2 (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)))) to the current goal.
Assume Hm3.
Apply (Hm3 (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)))) to the current goal.
Assume Hc1.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod R R = R.
An exact proof term for the current goal is (andEL (setprod R R = R) (Rlt a b) Hc1).
An exact proof term for the current goal is (setprod_R_R_neq_R Heq).
Assume Hc2.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod R R = rational_numbers.
An exact proof term for the current goal is (andEL (setprod R R = rational_numbers) (Rlt a b) Hc2).
An exact proof term for the current goal is (setprod_R_R_neq_rational_numbers Heq).
Assume Hc3.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod R R = ω.
An exact proof term for the current goal is (andEL (setprod R R = ω) (a ∈ b) Hc3).
An exact proof term for the current goal is (setprod_R_R_neq_omega Heq).
Assume Hc4.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod R R = ω ∖ {0}.
An exact proof term for the current goal is (andEL (setprod R R = ω ∖ {0}) (a ∈ b) Hc4).
An exact proof term for the current goal is (setprod_R_R_neq_omega_nonzero Heq).
Assume Hc5.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod R R = setprod 2 ω.
An exact proof term for the current goal is (andEL (setprod R R = setprod 2 ω) (∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) Hc5).
An exact proof term for the current goal is (setprod_R_R_neq_setprod_2_omega Heq).
Assume Hc6.
An exact proof term for the current goal is (andER (setprod R R = setprod R R) (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) Hc6).
Assume Hord: ordinal (setprod R R) ∧ setprod R R ≠ R ∧ setprod R R ≠ rational_numbers ∧ setprod R R ≠ setprod 2 ω ∧ setprod R R ≠ setprod R R ∧ a ∈ b.
Apply FalseE to the current goal.
Apply Hord to the current goal.
Assume Hcore Haeb.
Apply Hcore to the current goal.
Assume Hcore2 HneqRR.
We prove the intermediate claim Hrefl: setprod R R = setprod R R.
Use reflexivity.
An exact proof term for the current goal is (HneqRR Hrefl).
∎