Let a and b be given.
Assume Hrel: order_rel (setprod 2 ω) a b.
Apply (Hrel (∃i m j n : set, (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))))) to the current goal.
Assume Hleft6.
Apply (Hleft6 (∃i m j n : set, (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))))) to the current goal.
Assume Hleft.
Apply (Hleft (∃i m j n : set, (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))))) to the current goal.
Assume Hmid.
Apply (Hmid (∃i m j n : set, (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))))) to the current goal.
Assume Hm2.
Apply (Hm2 (∃i m j n : set, (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))))) to the current goal.
Assume Hm3.
Apply (Hm3 (∃i m j n : set, (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))))) to the current goal.
Assume Hc1.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod 2 ω = R.
An exact proof term for the current goal is (andEL (setprod 2 ω = R) (Rlt a b) Hc1).
An exact proof term for the current goal is (setprod_2_omega_neq_R Heq).
Assume Hc2.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod 2 ω = rational_numbers.
An exact proof term for the current goal is (andEL (setprod 2 ω = rational_numbers) (Rlt a b) Hc2).
An exact proof term for the current goal is (setprod_2_omega_neq_rational_numbers Heq).
Assume Hc3.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod 2 ω = ω.
An exact proof term for the current goal is (andEL (setprod 2 ω = ω) (a ∈ b) Hc3).
An exact proof term for the current goal is (setprod_2_omega_neq_omega Heq).
Assume Hc4.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod 2 ω = ω ∖ {0}.
An exact proof term for the current goal is (andEL (setprod 2 ω = ω ∖ {0}) (a ∈ b) Hc4).
An exact proof term for the current goal is (setprod_2_omega_neq_omega_nonzero Heq).
Assume Hc5.
An exact proof term for the current goal is (andER (setprod 2 ω = 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).
Assume Hc6.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: setprod 2 ω = setprod R R.
An exact proof term for the current goal is (andEL (setprod 2 ω = setprod R R) (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) Hc6).
An exact proof term for the current goal is (setprod_2_omega_neq_setprod_R_R Heq).
Assume Hord: ordinal (setprod 2 ω) ∧ setprod 2 ω ≠ R ∧ setprod 2 ω ≠ rational_numbers ∧ setprod 2 ω ≠ setprod 2 ω ∧ setprod 2 ω ≠ 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.
Apply Hcore2 to the current goal.
Assume Hcore3 HneqXX.
Apply Hcore3 to the current goal.
Assume Hcore4 HneqRat.
Apply Hcore4 to the current goal.
Assume HordX HneqR.
We prove the intermediate claim Hrefl: setprod 2 ω = setprod 2 ω.
Use reflexivity.
An exact proof term for the current goal is (HneqXX Hrefl).
∎