Let X, a, b and c be given.
Assume Hso HaX HbX HcX Hab Hbc.
Apply (xm (X = R)) to the current goal.
Assume HXR: X = R.
rewrite the current goal using HXR (from left to right).
We prove the intermediate claim HabR: order_rel R a b.
We will prove order_rel R a b.
rewrite the current goal using HXR (from right to left) at position 1.
An exact proof term for the current goal is Hab.
We prove the intermediate claim HbcR: order_rel R b c.
We will prove order_rel R b c.
rewrite the current goal using HXR (from right to left) at position 1.
An exact proof term for the current goal is Hbc.
We prove the intermediate claim Hablt: Rlt a b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt a b HabR).
We prove the intermediate claim Hbclt: Rlt b c.
An exact proof term for the current goal is (order_rel_R_implies_Rlt b c HbcR).
We prove the intermediate claim Haclt: Rlt a c.
An exact proof term for the current goal is (Rlt_tra a b c Hablt Hbclt).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a c Haclt).
Assume HneqR: ¬ (X = R).
Apply (xm (X = rational_numbers)) to the current goal.
Assume HXQ: X = rational_numbers.
rewrite the current goal using HXQ (from left to right).
We prove the intermediate claim HabQ: order_rel rational_numbers a b.
We will prove order_rel rational_numbers a b.
rewrite the current goal using HXQ (from right to left) at position 1.
An exact proof term for the current goal is Hab.
We prove the intermediate claim HbcQ: order_rel rational_numbers b c.
We will prove order_rel rational_numbers b c.
rewrite the current goal using HXQ (from right to left) at position 1.
An exact proof term for the current goal is Hbc.
We prove the intermediate claim Hm1Q: minus_SNo 1 ∈ rational_numbers.
We will prove minus_SNo 1 ∈ rational.
We prove the intermediate claim HdefQ: rational_numbers = rational.
Use reflexivity.
We prove the intermediate claim H1rat: 1 ∈ rational.
We prove the intermediate claim H1real: 1 ∈ real.
An exact proof term for the current goal is real_1.
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim H1int: 1 ∈ int.
An exact proof term for the current goal is (Subq_omega_int 1 H1omega).
We prove the intermediate claim H1not0: 1 ∉ {0}.
Assume H1: 1 ∈ {0}.
We will prove False.
We prove the intermediate claim Heq10: 1 = 0.
An exact proof term for the current goal is (SingE 0 1 H1).
An exact proof term for the current goal is (neq_1_0 Heq10).
We prove the intermediate claim H1nonzero: 1 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} 1 H1omega H1not0).
We prove the intermediate claim Hrecip1: recip_SNo 1 = 1.
We prove the intermediate claim H1neq0: 1 ≠ 0.
An exact proof term for the current goal is neq_1_0.
We prove the intermediate claim Hinv: mul_SNo 1 (recip_SNo 1) = 1.
An exact proof term for the current goal is (recip_SNo_invR 1 SNo_1 H1neq0).
rewrite the current goal using (mul_SNo_oneL (recip_SNo 1) (SNo_recip_SNo 1 SNo_1)) (from right to left) at position 1.
An exact proof term for the current goal is Hinv.
We prove the intermediate claim Heq1: 1 = div_SNo 1 1.
We prove the intermediate claim Hdivdef: div_SNo 1 1 = mul_SNo 1 (recip_SNo 1).
Use reflexivity.
rewrite the current goal using Hdivdef (from left to right).
rewrite the current goal using Hrecip1 (from left to right).
rewrite the current goal using (mul_SNo_oneR 1 SNo_1) (from left to right).
Use reflexivity.
We prove the intermediate claim Hex: ∃m ∈ int, ∃n ∈ ω ∖ {0}, 1 = div_SNo m n.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1int.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1nonzero.
An exact proof term for the current goal is Heq1.
An exact proof term for the current goal is (SepI real (λx : set ⇒ ∃m ∈ int, ∃n ∈ ω ∖ {0}, x = div_SNo m n) 1 H1real Hex).
We prove the intermediate claim Hm1rat: minus_SNo 1 ∈ rational.
An exact proof term for the current goal is (rational_minus_SNo 1 H1rat).
rewrite the current goal using HdefQ (from right to left) at position 1.
An exact proof term for the current goal is Hm1rat.
We prove the intermediate claim Hm1notomega: minus_SNo 1 ∉ ω.
Assume Hm1: minus_SNo 1 ∈ ω.
We will prove False.
We prove the intermediate claim Hle0: 0 ≤ minus_SNo 1.
An exact proof term for the current goal is (omega_nonneg (minus_SNo 1) Hm1).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
Apply (SNoLeE 0 (minus_SNo 1) SNo_0 Hm1S Hle0 False) to the current goal.
Assume H0ltm1: 0 < minus_SNo 1.
We prove the intermediate claim Hm1lt0: minus_SNo 1 < 0.
An exact proof term for the current goal is minus_1_lt_0.
We prove the intermediate claim H00: 0 < 0.
An exact proof term for the current goal is (SNoLt_tra 0 (minus_SNo 1) 0 SNo_0 Hm1S SNo_0 H0ltm1 Hm1lt0).
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
Assume H0eqm1: 0 = minus_SNo 1.
We prove the intermediate claim Hm1lt0: minus_SNo 1 < 0.
An exact proof term for the current goal is minus_1_lt_0.
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using H0eqm1 (from left to right) at position 1.
An exact proof term for the current goal is Hm1lt0.
An exact proof term for the current goal is ((SNoLt_irref 0) H00).
We prove the intermediate claim Hablt: Rlt a b.
Apply (HabQ (Rlt a b)) to the current goal.
Assume Hleft6.
Apply (Hleft6 (Rlt a b)) to the current goal.
Assume Hleft.
Apply (Hleft (Rlt a b)) to the current goal.
Assume Hleft2.
Apply (Hleft2 (Rlt a b)) to the current goal.
Assume Hleft3.
Apply (Hleft3 (Rlt a b)) to the current goal.
Assume Hleft4.
Apply (Hleft4 (Rlt a b)) to the current goal.
Assume HA: rational_numbers = R ∧ Rlt a b.
An exact proof term for the current goal is (andER (rational_numbers = R) (Rlt a b) HA).
Assume HB: rational_numbers = rational_numbers ∧ Rlt a b.
An exact proof term for the current goal is (andER (rational_numbers = rational_numbers) (Rlt a b) HB).
Assume HC: rational_numbers = ω ∧ a ∈ b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: rational_numbers = ω.
An exact proof term for the current goal is (andEL (rational_numbers = ω) (a ∈ b) HC).
We prove the intermediate claim Hm1omega: minus_SNo 1 ∈ ω.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hm1Q.
An exact proof term for the current goal is (Hm1notomega Hm1omega).
Assume HD: rational_numbers = ω ∖ {0} ∧ a ∈ b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: rational_numbers = ω ∖ {0}.
An exact proof term for the current goal is (andEL (rational_numbers = ω ∖ {0}) (a ∈ b) HD).
We prove the intermediate claim Hm1NZ: minus_SNo 1 ∈ ω ∖ {0}.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hm1Q.
We prove the intermediate claim Hm1omega: minus_SNo 1 ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} (minus_SNo 1) Hm1NZ).
An exact proof term for the current goal is (Hm1notomega Hm1omega).
Assume HE: rational_numbers = 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)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: rational_numbers = setprod 2 ω.
An exact proof term for the current goal is (andEL (rational_numbers = 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))) HE).
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Hp: (0,1) ∈ setprod 2 ω.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 1 In_0_2 H1omega).
We prove the intermediate claim HpQ: (0,1) ∈ rational_numbers.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hp.
We prove the intermediate claim HSingQ: {1} ∈ rational_numbers.
rewrite the current goal using tuple_0_1_eq_Sing1 (from right to left).
An exact proof term for the current goal is HpQ.
We prove the intermediate claim HSingR: {1} ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R {1} HSingQ).
We prove the intermediate claim HSingS: SNo {1}.
An exact proof term for the current goal is (real_SNo {1} HSingR).
An exact proof term for the current goal is (Sing1_not_SNo HSingS).
Assume HF: rational_numbers = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: rational_numbers = setprod R R.
An exact proof term for the current goal is (andEL (rational_numbers = setprod R R) (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) HF).
We prove the intermediate claim Heq': setprod R R = rational_numbers.
Use symmetry.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (setprod_R_R_neq_rational_numbers Heq').
Assume Hord: ordinal rational_numbers ∧ rational_numbers ≠ R ∧ rational_numbers ≠ rational_numbers ∧ rational_numbers ≠ setprod 2 ω ∧ rational_numbers ≠ 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 Hneq2omega.
Apply Hcore3 to the current goal.
Assume HordQ HneqQQ.
We prove the intermediate claim Hrefl: rational_numbers = rational_numbers.
Use reflexivity.
An exact proof term for the current goal is (HneqQQ Hrefl).
We prove the intermediate claim Hbclt: Rlt b c.
Apply (HbcQ (Rlt b c)) to the current goal.
Assume Hleft6.
Apply (Hleft6 (Rlt b c)) to the current goal.
Assume Hleft.
Apply (Hleft (Rlt b c)) to the current goal.
Assume Hleft2.
Apply (Hleft2 (Rlt b c)) to the current goal.
Assume Hleft3.
Apply (Hleft3 (Rlt b c)) to the current goal.
Assume Hleft4.
Apply (Hleft4 (Rlt b c)) to the current goal.
Assume HA: rational_numbers = R ∧ Rlt b c.
An exact proof term for the current goal is (andER (rational_numbers = R) (Rlt b c) HA).
Assume HB: rational_numbers = rational_numbers ∧ Rlt b c.
An exact proof term for the current goal is (andER (rational_numbers = rational_numbers) (Rlt b c) HB).
Assume HC: rational_numbers = ω ∧ b ∈ c.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: rational_numbers = ω.
An exact proof term for the current goal is (andEL (rational_numbers = ω) (b ∈ c) HC).
We prove the intermediate claim Hm1omega: minus_SNo 1 ∈ ω.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hm1Q.
An exact proof term for the current goal is (Hm1notomega Hm1omega).
Assume HD: rational_numbers = ω ∖ {0} ∧ b ∈ c.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: rational_numbers = ω ∖ {0}.
An exact proof term for the current goal is (andEL (rational_numbers = ω ∖ {0}) (b ∈ c) HD).
We prove the intermediate claim Hm1NZ: minus_SNo 1 ∈ ω ∖ {0}.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hm1Q.
We prove the intermediate claim Hm1omega: minus_SNo 1 ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} (minus_SNo 1) Hm1NZ).
An exact proof term for the current goal is (Hm1notomega Hm1omega).
Assume HE: rational_numbers = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ b = (i,m) ∧ c = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: rational_numbers = setprod 2 ω.
An exact proof term for the current goal is (andEL (rational_numbers = setprod 2 ω) (∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ b = (i,m) ∧ c = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) HE).
We prove the intermediate claim H1omega: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Hp: (0,1) ∈ setprod 2 ω.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 1 In_0_2 H1omega).
We prove the intermediate claim HpQ: (0,1) ∈ rational_numbers.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hp.
We prove the intermediate claim HSingQ: {1} ∈ rational_numbers.
rewrite the current goal using tuple_0_1_eq_Sing1 (from right to left).
An exact proof term for the current goal is HpQ.
We prove the intermediate claim HSingR: {1} ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R {1} HSingQ).
We prove the intermediate claim HSingS: SNo {1}.
An exact proof term for the current goal is (real_SNo {1} HSingR).
An exact proof term for the current goal is (Sing1_not_SNo HSingS).
Assume HF: rational_numbers = setprod R R ∧ ∃a1 a2 b1 b2 : set, b = (a1,a2) ∧ c = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: rational_numbers = setprod R R.
An exact proof term for the current goal is (andEL (rational_numbers = setprod R R) (∃a1 a2 b1 b2 : set, b = (a1,a2) ∧ c = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) HF).
We prove the intermediate claim Heq': setprod R R = rational_numbers.
Use symmetry.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (setprod_R_R_neq_rational_numbers Heq').
Assume Hord: ordinal rational_numbers ∧ rational_numbers ≠ R ∧ rational_numbers ≠ rational_numbers ∧ rational_numbers ≠ setprod 2 ω ∧ rational_numbers ≠ setprod R R ∧ b ∈ c.
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 Hneq2omega.
Apply Hcore3 to the current goal.
Assume HordQ HneqQQ.
We prove the intermediate claim Hrefl: rational_numbers = rational_numbers.
Use reflexivity.
An exact proof term for the current goal is (HneqQQ Hrefl).
We prove the intermediate claim Haclt: Rlt a c.
An exact proof term for the current goal is (Rlt_tra a b c Hablt Hbclt).
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a c Haclt).
Assume HneqQ: ¬ (X = rational_numbers).
Apply (xm (X = ω)) to the current goal.
Assume HXo: X = ω.
rewrite the current goal using HXo (from left to right).
We prove the intermediate claim HabO: order_rel ω a b.
We will prove order_rel ω a b.
rewrite the current goal using HXo (from right to left) at position 1.
An exact proof term for the current goal is Hab.
We prove the intermediate claim HbcO: order_rel ω b c.
We will prove order_rel ω b c.
rewrite the current goal using HXo (from right to left) at position 1.
An exact proof term for the current goal is Hbc.
We prove the intermediate claim Habmem: a ∈ b.
An exact proof term for the current goal is (order_rel_omega_implies_mem a b HabO).
We prove the intermediate claim Hbcmem: b ∈ c.
An exact proof term for the current goal is (order_rel_omega_implies_mem b c HbcO).
We prove the intermediate claim HcOmega: c ∈ ω.
rewrite the current goal using HXo (from right to left) at position 1.
An exact proof term for the current goal is HcX.
We prove the intermediate claim HcNat: nat_p c.
An exact proof term for the current goal is (omega_nat_p c HcOmega).
We prove the intermediate claim HcOrd: ordinal c.
An exact proof term for the current goal is (nat_p_ordinal c HcNat).
We prove the intermediate claim HcTr: TransSet c.
An exact proof term for the current goal is (ordinal_TransSet c HcOrd).
We prove the intermediate claim HbSubc: b ⊆ c.
An exact proof term for the current goal is (HcTr b Hbcmem).
We prove the intermediate claim Hacmem: a ∈ c.
An exact proof term for the current goal is (HbSubc a Habmem).
An exact proof term for the current goal is (mem_implies_order_rel_omega a c Hacmem).
Assume HneqO: ¬ (X = ω).
Apply (xm (X = ω ∖ {0})) to the current goal.
Assume HXnz: X = ω ∖ {0}.
rewrite the current goal using HXnz (from left to right).
We prove the intermediate claim HabNz: order_rel (ω ∖ {0}) a b.
We will prove order_rel (ω ∖ {0}) a b.
rewrite the current goal using HXnz (from right to left) at position 1.
An exact proof term for the current goal is Hab.
We prove the intermediate claim HbcNz: order_rel (ω ∖ {0}) b c.
We will prove order_rel (ω ∖ {0}) b c.
rewrite the current goal using HXnz (from right to left) at position 1.
An exact proof term for the current goal is Hbc.
We prove the intermediate claim Habmem: a ∈ b.
An exact proof term for the current goal is (order_rel_omega_nonzero_implies_mem a b HabNz).
We prove the intermediate claim Hbcmem: b ∈ c.
An exact proof term for the current goal is (order_rel_omega_nonzero_implies_mem b c HbcNz).
We prove the intermediate claim HcNZ: c ∈ ω ∖ {0}.
rewrite the current goal using HXnz (from right to left) at position 1.
An exact proof term for the current goal is HcX.
We prove the intermediate claim HcOmega: c ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} c HcNZ).
We prove the intermediate claim HcNat: nat_p c.
An exact proof term for the current goal is (omega_nat_p c HcOmega).
We prove the intermediate claim HcOrd: ordinal c.
An exact proof term for the current goal is (nat_p_ordinal c HcNat).
We prove the intermediate claim HcTr: TransSet c.
An exact proof term for the current goal is (ordinal_TransSet c HcOrd).
We prove the intermediate claim HbSubc: b ⊆ c.
An exact proof term for the current goal is (HcTr b Hbcmem).
We prove the intermediate claim Hacmem: a ∈ c.
An exact proof term for the current goal is (HbSubc a Habmem).
An exact proof term for the current goal is (mem_implies_order_rel_omega_nonzero a c Hacmem).
Assume HneqNz: ¬ (X = ω ∖ {0}).
Apply (xm (X = setprod 2 ω)) to the current goal.
Assume HX2: X = setprod 2 ω.
rewrite the current goal using HX2 (from left to right).
We prove the intermediate claim Hab2: order_rel (setprod 2 ω) a b.
We will prove order_rel (setprod 2 ω) a b.
rewrite the current goal using HX2 (from right to left) at position 1.
An exact proof term for the current goal is Hab.
We prove the intermediate claim Hbc2: order_rel (setprod 2 ω) b c.
We will prove order_rel (setprod 2 ω) b c.
rewrite the current goal using HX2 (from right to left) at position 1.
An exact proof term for the current goal is Hbc.
We prove the intermediate claim Hexab: ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)).
Apply (Hab2 (∃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: setprod 2 ω = R ∧ Rlt a b.
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).
We prove the intermediate claim HXR: X = R.
rewrite the current goal using HX2 (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqR HXR).
Assume Hc2: setprod 2 ω = rational_numbers ∧ Rlt a b.
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).
We prove the intermediate claim HXQ2: X = rational_numbers.
rewrite the current goal using HX2 (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqQ HXQ2).
Assume Hc3: setprod 2 ω = ω ∧ a ∈ b.
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).
We prove the intermediate claim HXo2: X = ω.
rewrite the current goal using HX2 (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqO HXo2).
Assume Hc4: setprod 2 ω = ω ∖ {0} ∧ a ∈ b.
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).
We prove the intermediate claim HXnz2: X = ω ∖ {0}.
rewrite the current goal using HX2 (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqNz HXnz2).
Assume Hc5: 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)).
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: setprod 2 ω = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
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).
We prove the intermediate claim Heq2: setprod R R = setprod 2 ω.
Use symmetry.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (setprod_R_R_neq_setprod_2_omega Heq2).
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.
We prove the intermediate claim Hrefl: setprod 2 ω = setprod 2 ω.
Use reflexivity.
An exact proof term for the current goal is (HneqXX Hrefl).
We prove the intermediate claim Hexbc: ∃j2 n2 k p : set, j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p) ∧ (j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p)).
Apply (Hbc2 (∃j2 n2 k p : set, (j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p) ∧ (j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p))))) to the current goal.
Assume Hleft6.
Apply (Hleft6 (∃j2 n2 k p : set, (j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p) ∧ (j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p))))) to the current goal.
Assume Hleft.
Apply (Hleft (∃j2 n2 k p : set, (j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p) ∧ (j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p))))) to the current goal.
Assume Hmid.
Apply (Hmid (∃j2 n2 k p : set, (j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p) ∧ (j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p))))) to the current goal.
Assume Hm2.
Apply (Hm2 (∃j2 n2 k p : set, (j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p) ∧ (j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p))))) to the current goal.
Assume Hm3.
Apply (Hm3 (∃j2 n2 k p : set, (j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p) ∧ (j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p))))) to the current goal.
Assume Hc1: setprod 2 ω = R ∧ Rlt b c.
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 b c) Hc1).
We prove the intermediate claim HXR: X = R.
rewrite the current goal using HX2 (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqR HXR).
Assume Hc2: setprod 2 ω = rational_numbers ∧ Rlt b c.
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 b c) Hc2).
We prove the intermediate claim HXQ2: X = rational_numbers.
rewrite the current goal using HX2 (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqQ HXQ2).
Assume Hc3: setprod 2 ω = ω ∧ b ∈ c.
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 ω = ω) (b ∈ c) Hc3).
We prove the intermediate claim HXo2: X = ω.
rewrite the current goal using HX2 (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqO HXo2).
Assume Hc4: setprod 2 ω = ω ∖ {0} ∧ b ∈ c.
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}) (b ∈ c) Hc4).
We prove the intermediate claim HXnz2: X = ω ∖ {0}.
rewrite the current goal using HX2 (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqNz HXnz2).
Assume Hc5: setprod 2 ω = setprod 2 ω ∧ ∃j2 n2 k p : set, j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p) ∧ (j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p)).
An exact proof term for the current goal is (andER (setprod 2 ω = setprod 2 ω) (∃j2 n2 k p : set, j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p) ∧ (j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p))) Hc5).
Assume Hc6: setprod 2 ω = setprod R R ∧ ∃a1 a2 b1 b2 : set, b = (a1,a2) ∧ c = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
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, b = (a1,a2) ∧ c = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) Hc6).
We prove the intermediate claim Heq2: setprod R R = setprod 2 ω.
Use symmetry.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (setprod_R_R_neq_setprod_2_omega Heq2).
Assume Hord: ordinal (setprod 2 ω) ∧ setprod 2 ω ≠ R ∧ setprod 2 ω ≠ rational_numbers ∧ setprod 2 ω ≠ setprod 2 ω ∧ setprod 2 ω ≠ setprod R R ∧ b ∈ c.
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.
We prove the intermediate claim Hrefl: setprod 2 ω = setprod 2 ω.
Use reflexivity.
An exact proof term for the current goal is (HneqXX Hrefl).
Apply Hexab to the current goal.
Let i be given.
Assume HiPair.
Apply HiPair to the current goal.
Let m be given.
Assume HmPair.
Apply HmPair to the current goal.
Let j be given.
Assume HjPair.
Apply HjPair to the current goal.
Let n be given.
Assume HabCore.
Apply Hexbc to the current goal.
Let j2 be given.
Assume Hj2Pair.
Apply Hj2Pair to the current goal.
Let n2 be given.
Assume Hn2Pair.
Apply Hn2Pair to the current goal.
Let k be given.
Assume HkPair.
Apply HkPair to the current goal.
Let p be given.
Assume HbcCore.
We prove the intermediate claim HabCoords: (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n)).
Apply HabCore to the current goal.
Assume Hc0 Hlex0.
An exact proof term for the current goal is Hc0.
We prove the intermediate claim HabLex: i ∈ j ∨ (i = j ∧ m ∈ n).
Apply HabCore to the current goal.
Assume Hc0 Hlex0.
An exact proof term for the current goal is Hlex0.
We prove the intermediate claim HbcCoords: (j2 ∈ 2 ∧ n2 ∈ ω ∧ k ∈ 2 ∧ p ∈ ω ∧ b = (j2,n2) ∧ c = (k,p)).
Apply HbcCore to the current goal.
Assume Hc0 Hlex0.
An exact proof term for the current goal is Hc0.
We prove the intermediate claim HbcLex: j2 ∈ k ∨ (j2 = k ∧ n2 ∈ p).
Apply HbcCore to the current goal.
Assume Hc0 Hlex0.
An exact proof term for the current goal is Hlex0.
We prove the intermediate claim Hbeq1: b = (j,n).
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m)) (b = (j,n)) HabCoords).
We prove the intermediate claim HbEq2: b = (j2,n2).
Set T0 to be the term ((((j2 ∈ 2 ∧ n2 ∈ ω) ∧ k ∈ 2) ∧ p ∈ ω) ∧ b = (j2,n2)).
Set T1 to be the term (((j2 ∈ 2 ∧ n2 ∈ ω) ∧ k ∈ 2) ∧ p ∈ ω).
We prove the intermediate claim Hbc0: T0.
An exact proof term for the current goal is (andEL T0 (c = (k,p)) HbcCoords).
An exact proof term for the current goal is (andER T1 (b = (j2,n2)) Hbc0).
We prove the intermediate claim HbEqTuples: (j,n) = (j2,n2).
rewrite the current goal using Hbeq1 (from right to left) at position 1.
An exact proof term for the current goal is HbEq2.
We prove the intermediate claim Hjjn: j = j2 ∧ n = n2.
An exact proof term for the current goal is (tuple_eq_coords j n j2 n2 HbEqTuples).
We prove the intermediate claim Hjj: j = j2.
An exact proof term for the current goal is (andEL (j = j2) (n = n2) Hjjn).
We prove the intermediate claim Hnn: n = n2.
An exact proof term for the current goal is (andER (j = j2) (n = n2) Hjjn).
Set HabT0 to be the term (i ∈ 2 ∧ m ∈ ω).
Set HabT1 to be the term (HabT0 ∧ j ∈ 2).
Set HabT2 to be the term (HabT1 ∧ n ∈ ω).
Set HabT3 to be the term (HabT2 ∧ a = (i,m)).
Set HabT4 to be the term (HabT3 ∧ b = (j,n)).
Set HbcT0 to be the term (j2 ∈ 2 ∧ n2 ∈ ω).
Set HbcT1 to be the term (HbcT0 ∧ k ∈ 2).
Set HbcT2 to be the term (HbcT1 ∧ p ∈ ω).
Set HbcT3 to be the term (HbcT2 ∧ b = (j2,n2)).
Set HbcT4 to be the term (HbcT3 ∧ c = (k,p)).
We prove the intermediate claim Hab3: HabT3.
An exact proof term for the current goal is (andEL HabT3 (b = (j,n)) HabCoords).
We prove the intermediate claim Hab2: HabT2.
An exact proof term for the current goal is (andEL HabT2 (a = (i,m)) Hab3).
We prove the intermediate claim Hab1: HabT1.
An exact proof term for the current goal is (andEL HabT1 (n ∈ ω) Hab2).
We prove the intermediate claim Hab0: HabT0.
An exact proof term for the current goal is (andEL HabT0 (j ∈ 2) Hab1).
We prove the intermediate claim Hi2: i ∈ 2.
An exact proof term for the current goal is (andEL (i ∈ 2) (m ∈ ω) Hab0).
We prove the intermediate claim HmO: m ∈ ω.
An exact proof term for the current goal is (andER (i ∈ 2) (m ∈ ω) Hab0).
We prove the intermediate claim Hbc3: HbcT3.
An exact proof term for the current goal is (andEL HbcT3 (c = (k,p)) HbcCoords).
We prove the intermediate claim Hbc2: HbcT2.
An exact proof term for the current goal is (andEL HbcT2 (b = (j2,n2)) Hbc3).
We prove the intermediate claim Hbc1: HbcT1.
An exact proof term for the current goal is (andEL HbcT1 (p ∈ ω) Hbc2).
We prove the intermediate claim Hbc0: HbcT0.
An exact proof term for the current goal is (andEL HbcT0 (k ∈ 2) Hbc1).
We prove the intermediate claim Hj2in: j2 ∈ 2.
An exact proof term for the current goal is (andEL (j2 ∈ 2) (n2 ∈ ω) Hbc0).
We prove the intermediate claim Hk2: k ∈ 2.
An exact proof term for the current goal is (andER HbcT0 (k ∈ 2) Hbc1).
We prove the intermediate claim HpO: p ∈ ω.
An exact proof term for the current goal is (andER HbcT1 (p ∈ ω) Hbc2).
We prove the intermediate claim HaEq: a = (i,m).
An exact proof term for the current goal is (andER HabT2 (a = (i,m)) Hab3).
We prove the intermediate claim HcEq: c = (k,p).
An exact proof term for the current goal is (andER HbcT3 (c = (k,p)) HbcCoords).
We prove the intermediate claim Hj2kLex: j ∈ k ∨ (j = k ∧ n ∈ p).
rewrite the current goal using Hjj (from left to right).
rewrite the current goal using Hnn (from left to right).
An exact proof term for the current goal is HbcLex.
We prove the intermediate claim Hcmp: i ∈ k ∨ (i = k ∧ m ∈ p).
Apply (HabLex (i ∈ k ∨ (i = k ∧ m ∈ p))) to the current goal.
Assume Hij: i ∈ j.
Apply (Hj2kLex (i ∈ k ∨ (i = k ∧ m ∈ p))) to the current goal.
Assume Hjk: j ∈ k.
Apply orIL to the current goal.
We prove the intermediate claim H2ord: ordinal 2.
An exact proof term for the current goal is ordinal_2.
We prove the intermediate claim HkOrd: ordinal k.
An exact proof term for the current goal is (ordinal_Hered 2 H2ord k Hk2).
We prove the intermediate claim HkTr: TransSet k.
An exact proof term for the current goal is (ordinal_TransSet k HkOrd).
We prove the intermediate claim HjSubk: j ⊆ k.
An exact proof term for the current goal is (HkTr j Hjk).
An exact proof term for the current goal is (HjSubk i Hij).
Assume Hjkeq: j = k ∧ n ∈ p.
Apply orIL to the current goal.
We prove the intermediate claim Hjk: j = k.
An exact proof term for the current goal is (andEL (j = k) (n ∈ p) Hjkeq).
rewrite the current goal using Hjk (from right to left).
An exact proof term for the current goal is Hij.
Assume Hijeq: i = j ∧ m ∈ n.
We prove the intermediate claim HijEq: i = j.
An exact proof term for the current goal is (andEL (i = j) (m ∈ n) Hijeq).
We prove the intermediate claim Hmn: m ∈ n.
An exact proof term for the current goal is (andER (i = j) (m ∈ n) Hijeq).
Apply (Hj2kLex (i ∈ k ∨ (i = k ∧ m ∈ p))) to the current goal.
Assume Hjk: j ∈ k.
Apply orIL to the current goal.
rewrite the current goal using HijEq (from left to right).
An exact proof term for the current goal is Hjk.
Assume Hjkeq: j = k ∧ n ∈ p.
We prove the intermediate claim HjkEq: j = k.
An exact proof term for the current goal is (andEL (j = k) (n ∈ p) Hjkeq).
We prove the intermediate claim Hnp: n ∈ p.
An exact proof term for the current goal is (andER (j = k) (n ∈ p) Hjkeq).
Apply orIR to the current goal.
Apply andI to the current goal.
rewrite the current goal using HijEq (from left to right).
An exact proof term for the current goal is HjkEq.
We prove the intermediate claim HpNat: nat_p p.
An exact proof term for the current goal is (omega_nat_p p HpO).
We prove the intermediate claim HpOrd: ordinal p.
An exact proof term for the current goal is (nat_p_ordinal p HpNat).
We prove the intermediate claim HpTr: TransSet p.
An exact proof term for the current goal is (ordinal_TransSet p HpOrd).
We prove the intermediate claim HnSubp: n ⊆ p.
An exact proof term for the current goal is (HpTr n Hnp).
An exact proof term for the current goal is (HnSubp m Hmn).
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_2_omega_intro i m k p Hi2 HmO Hk2 HpO Hcmp).
Assume Hneq2: ¬ (X = setprod 2 ω).
Apply (xm (X = setprod R R)) to the current goal.
Assume HXRR: X = setprod R R.
rewrite the current goal using HXRR (from left to right).
We prove the intermediate claim HabRR: order_rel (setprod R R) a b.
We will prove order_rel (setprod R R) a b.
rewrite the current goal using HXRR (from right to left) at position 1.
An exact proof term for the current goal is Hab.
We prove the intermediate claim HbcRR: order_rel (setprod R R) b c.
We will prove order_rel (setprod R R) b c.
rewrite the current goal using HXRR (from right to left) at position 1.
An exact proof term for the current goal is Hbc.
We prove the intermediate claim Hexab: ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
Apply (HabRR (∃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 Hleft2.
Apply (Hleft2 (∃a1 a2 b1 b2 : set, (a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))))) to the current goal.
Assume Hleft3.
Apply (Hleft3 (∃a1 a2 b1 b2 : set, (a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))))) to the current goal.
Assume Hleft4.
Apply (Hleft4 (∃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: setprod R R = R ∧ Rlt a b.
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).
We prove the intermediate claim HXR: X = R.
rewrite the current goal using HXRR (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqR HXR).
Assume Hc2: setprod R R = rational_numbers ∧ Rlt a b.
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).
We prove the intermediate claim HXQ2: X = rational_numbers.
rewrite the current goal using HXRR (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqQ HXQ2).
Assume Hc3: setprod R R = ω ∧ a ∈ b.
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).
We prove the intermediate claim HXo2: X = ω.
rewrite the current goal using HXRR (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqO HXo2).
Assume Hc4: setprod R R = ω ∖ {0} ∧ a ∈ b.
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).
We prove the intermediate claim HXnz2: X = ω ∖ {0}.
rewrite the current goal using HXRR (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqNz HXnz2).
Assume Hc5: 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))).
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: 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)).
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).
We prove the intermediate claim Hexbc: ∃b1 b2 c1 c2 : set, b = (b1,b2) ∧ c = (c1,c2) ∧ (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2)).
Apply (HbcRR (∃b1 b2 c1 c2 : set, (b = (b1,b2) ∧ c = (c1,c2) ∧ (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2))))) to the current goal.
Assume Hleft6.
Apply (Hleft6 (∃b1 b2 c1 c2 : set, (b = (b1,b2) ∧ c = (c1,c2) ∧ (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2))))) to the current goal.
Assume Hleft.
Apply (Hleft (∃b1 b2 c1 c2 : set, (b = (b1,b2) ∧ c = (c1,c2) ∧ (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2))))) to the current goal.
Assume Hleft2.
Apply (Hleft2 (∃b1 b2 c1 c2 : set, (b = (b1,b2) ∧ c = (c1,c2) ∧ (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2))))) to the current goal.
Assume Hleft3.
Apply (Hleft3 (∃b1 b2 c1 c2 : set, (b = (b1,b2) ∧ c = (c1,c2) ∧ (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2))))) to the current goal.
Assume Hleft4.
Apply (Hleft4 (∃b1 b2 c1 c2 : set, (b = (b1,b2) ∧ c = (c1,c2) ∧ (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2))))) to the current goal.
Assume Hc1: setprod R R = R ∧ Rlt b c.
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 b c) Hc1).
We prove the intermediate claim HXR: X = R.
rewrite the current goal using HXRR (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqR HXR).
Assume Hc2: setprod R R = rational_numbers ∧ Rlt b c.
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 b c) Hc2).
We prove the intermediate claim HXQ2: X = rational_numbers.
rewrite the current goal using HXRR (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqQ HXQ2).
Assume Hc3: setprod R R = ω ∧ b ∈ c.
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 = ω) (b ∈ c) Hc3).
We prove the intermediate claim HXo2: X = ω.
rewrite the current goal using HXRR (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqO HXo2).
Assume Hc4: setprod R R = ω ∖ {0} ∧ b ∈ c.
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}) (b ∈ c) Hc4).
We prove the intermediate claim HXnz2: X = ω ∖ {0}.
rewrite the current goal using HXRR (from left to right) at position 1.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (HneqNz HXnz2).
Assume Hc5: setprod R R = setprod 2 ω ∧ ∃i m j n : set, (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ b = (i,m) ∧ c = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))).
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 ∈ ω ∧ b = (i,m) ∧ c = (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: setprod R R = setprod R R ∧ ∃b1 b2 c1 c2 : set, b = (b1,b2) ∧ c = (c1,c2) ∧ (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2)).
An exact proof term for the current goal is (andER (setprod R R = setprod R R) (∃b1 b2 c1 c2 : set, b = (b1,b2) ∧ c = (c1,c2) ∧ (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2))) 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 ∧ b ∈ c.
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).
Apply Hexab to the current goal.
Let a1 be given.
Assume Ha1Pair.
Apply Ha1Pair to the current goal.
Let a2 be given.
Assume Ha2Pair.
Apply Ha2Pair to the current goal.
Let b1 be given.
Assume Hb1Pair.
Apply Hb1Pair to the current goal.
Let b2 be given.
Assume HabCore.
Apply Hexbc to the current goal.
Let b1x be given.
Assume Hb1xPair.
Apply Hb1xPair to the current goal.
Let b2x be given.
Assume Hb2xPair.
Apply Hb2xPair to the current goal.
Let c1 be given.
Assume Hc1Pair.
Apply Hc1Pair to the current goal.
Let c2 be given.
Assume HbcCore.
We prove the intermediate claim HabCoords: a = (a1,a2) ∧ b = (b1,b2).
An exact proof term for the current goal is (andEL (a = (a1,a2) ∧ b = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) HabCore).
We prove the intermediate claim HabCmp: Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2).
An exact proof term for the current goal is (andER (a = (a1,a2) ∧ b = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) HabCore).
We prove the intermediate claim HbcCoords: b = (b1x,b2x) ∧ c = (c1,c2).
An exact proof term for the current goal is (andEL (b = (b1x,b2x) ∧ c = (c1,c2)) (Rlt b1x c1 ∨ (b1x = c1 ∧ Rlt b2x c2)) HbcCore).
We prove the intermediate claim HbcCmp: Rlt b1x c1 ∨ (b1x = c1 ∧ Rlt b2x c2).
An exact proof term for the current goal is (andER (b = (b1x,b2x) ∧ c = (c1,c2)) (Rlt b1x c1 ∨ (b1x = c1 ∧ Rlt b2x c2)) HbcCore).
We prove the intermediate claim HbEqTuples: (b1,b2) = (b1x,b2x).
We prove the intermediate claim HbEq1: b = (b1,b2).
An exact proof term for the current goal is (andER (a = (a1,a2)) (b = (b1,b2)) HabCoords).
We prove the intermediate claim HbEq2: b = (b1x,b2x).
An exact proof term for the current goal is (andEL (b = (b1x,b2x)) (c = (c1,c2)) HbcCoords).
rewrite the current goal using HbEq1 (from right to left) at position 1.
An exact proof term for the current goal is HbEq2.
We prove the intermediate claim Hbcoords: b1 = b1x ∧ b2 = b2x.
An exact proof term for the current goal is (tuple_eq_coords b1 b2 b1x b2x HbEqTuples).
We prove the intermediate claim Hb1eq: b1 = b1x.
An exact proof term for the current goal is (andEL (b1 = b1x) (b2 = b2x) Hbcoords).
We prove the intermediate claim Hb2eq: b2 = b2x.
An exact proof term for the current goal is (andER (b1 = b1x) (b2 = b2x) Hbcoords).
We prove the intermediate claim HbcCmp2: Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2).
Apply (HbcCmp (Rlt b1 c1 ∨ (b1 = c1 ∧ Rlt b2 c2))) to the current goal.
Assume Hb1xc1: Rlt b1x c1.
Apply orIL to the current goal.
rewrite the current goal using Hb1eq (from left to right) at position 1.
An exact proof term for the current goal is Hb1xc1.
Assume Hb1xeq: b1x = c1 ∧ Rlt b2x c2.
We prove the intermediate claim Hb1xeq2: b1x = c1.
An exact proof term for the current goal is (andEL (b1x = c1) (Rlt b2x c2) Hb1xeq).
We prove the intermediate claim Hb2xlt: Rlt b2x c2.
An exact proof term for the current goal is (andER (b1x = c1) (Rlt b2x c2) Hb1xeq).
Apply orIR to the current goal.
Apply andI to the current goal.
rewrite the current goal using Hb1eq (from left to right) at position 1.
An exact proof term for the current goal is Hb1xeq2.
rewrite the current goal using Hb2eq (from left to right) at position 1.
An exact proof term for the current goal is Hb2xlt.
We prove the intermediate claim HacCmp: Rlt a1 c1 ∨ (a1 = c1 ∧ Rlt a2 c2).
Apply (HabCmp (Rlt a1 c1 ∨ (a1 = c1 ∧ Rlt a2 c2))) to the current goal.
Assume Ha1b1: Rlt a1 b1.
Apply (HbcCmp2 (Rlt a1 c1 ∨ (a1 = c1 ∧ Rlt a2 c2))) to the current goal.
Assume Hb1c1: Rlt b1 c1.
Apply orIL to the current goal.
An exact proof term for the current goal is (Rlt_tra a1 b1 c1 Ha1b1 Hb1c1).
Assume Hb1eqc1: b1 = c1 ∧ Rlt b2 c2.
Apply orIL to the current goal.
We prove the intermediate claim Hb1eq2: b1 = c1.
An exact proof term for the current goal is (andEL (b1 = c1) (Rlt b2 c2) Hb1eqc1).
rewrite the current goal using Hb1eq2 (from right to left).
An exact proof term for the current goal is Ha1b1.
Assume Ha1eqb1: a1 = b1 ∧ Rlt a2 b2.
We prove the intermediate claim Ha1eq: a1 = b1.
An exact proof term for the current goal is (andEL (a1 = b1) (Rlt a2 b2) Ha1eqb1).
We prove the intermediate claim Ha2lt: Rlt a2 b2.
An exact proof term for the current goal is (andER (a1 = b1) (Rlt a2 b2) Ha1eqb1).
Apply (HbcCmp2 (Rlt a1 c1 ∨ (a1 = c1 ∧ Rlt a2 c2))) to the current goal.
Assume Hb1c1: Rlt b1 c1.
Apply orIL to the current goal.
rewrite the current goal using Ha1eq (from left to right).
An exact proof term for the current goal is Hb1c1.
Assume Hb1eqc1: b1 = c1 ∧ Rlt b2 c2.
We prove the intermediate claim Hb1eq2: b1 = c1.
An exact proof term for the current goal is (andEL (b1 = c1) (Rlt b2 c2) Hb1eqc1).
We prove the intermediate claim Hb2lt: Rlt b2 c2.
An exact proof term for the current goal is (andER (b1 = c1) (Rlt b2 c2) Hb1eqc1).
Apply orIR to the current goal.
Apply andI to the current goal.
rewrite the current goal using Ha1eq (from left to right).
An exact proof term for the current goal is Hb1eq2.
An exact proof term for the current goal is (Rlt_tra a2 b2 c2 Ha2lt Hb2lt).
We prove the intermediate claim HaEq: a = (a1,a2).
An exact proof term for the current goal is (andEL (a = (a1,a2)) (b = (b1,b2)) HabCoords).
We prove the intermediate claim HcEq: c = (c1,c2).
An exact proof term for the current goal is (andER (b = (b1x,b2x)) (c = (c1,c2)) HbcCoords).
rewrite the current goal using HaEq (from left to right).
rewrite the current goal using HcEq (from left to right).
We will prove order_rel (setprod R R) (a1,a2) (c1,c2).
We will prove (setprod R R = R ∧ Rlt (a1,a2) (c1,c2)) ∨ (setprod R R = rational_numbers ∧ Rlt (a1,a2) (c1,c2)) ∨ (setprod R R = ω ∧ (a1,a2) ∈ (c1,c2)) ∨ (setprod R R = ω ∖ {0} ∧ (a1,a2) ∈ (c1,c2)) ∨ (setprod R R = setprod 2 ω ∧ ∃i m j n : set, (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (a1,a2) = (i,m) ∧ (c1,c2) = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)))) ∨ (setprod R R = setprod R R ∧ ∃x1 x2 y1 y2 : set, (a1,a2) = (x1,x2) ∧ (c1,c2) = (y1,y2) ∧ (Rlt x1 y1 ∨ (x1 = y1 ∧ Rlt x2 y2))) ∨ (ordinal (setprod R R) ∧ setprod R R ≠ R ∧ setprod R R ≠ rational_numbers ∧ setprod R R ≠ setprod 2 ω ∧ setprod R R ≠ setprod R R ∧ (a1,a2) ∈ (c1,c2)).
Apply orIL to the current goal.
Apply orIR to the current goal.
We will prove setprod R R = setprod R R ∧ ∃x1 x2 y1 y2 : set, (a1,a2) = (x1,x2) ∧ (c1,c2) = (y1,y2) ∧ (Rlt x1 y1 ∨ (x1 = y1 ∧ Rlt x2 y2)).
Apply andI to the current goal.
Use reflexivity.
We use a1 to witness the existential quantifier.
We use a2 to witness the existential quantifier.
We use c1 to witness the existential quantifier.
We use c2 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Use reflexivity.
Use reflexivity.
An exact proof term for the current goal is HacCmp.
Assume HneqRR: ¬ (X = setprod R R).
We prove the intermediate claim HordX: ordinal X.
Apply Hso to the current goal.
Assume Hleft6.
Apply Hleft6 to the current goal.
Assume Hleft5.
Apply Hleft5 to the current goal.
Assume Hleft4.
Apply Hleft4 to the current goal.
Assume Hleft3.
Apply Hleft3 to the current goal.
Assume Hleft2.
Apply Hleft2 to the current goal.
Assume HXeq: X = R.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqR HXeq).
Assume HXeq: X = rational_numbers.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqQ HXeq).
Assume HXeq: X = ω.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqO HXeq).
Assume HXeq: X = ω ∖ {0}.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqNz HXeq).
Assume HXeq: X = setprod 2 ω.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq2 HXeq).
Assume HXeq: X = setprod R R.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HneqRR HXeq).
Assume Hord.
An exact proof term for the current goal is Hord.
We prove the intermediate claim Habmem: a ∈ b.
Apply (Hab (a ∈ b)) to the current goal.
Assume Hleft6.
Apply (Hleft6 (a ∈ b)) to the current goal.
Assume Hleft5.
Apply (Hleft5 (a ∈ b)) to the current goal.
Assume Hleft4.
Apply (Hleft4 (a ∈ b)) to the current goal.
Assume Hleft3.
Apply (Hleft3 (a ∈ b)) to the current goal.
Assume Hleft2.
Apply (Hleft2 (a ∈ b)) to the current goal.
Assume Hc1: X = R ∧ Rlt a b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = R.
An exact proof term for the current goal is (andEL (X = R) (Rlt a b) Hc1).
An exact proof term for the current goal is (HneqR Heq).
Assume Hc2: X = rational_numbers ∧ Rlt a b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = rational_numbers.
An exact proof term for the current goal is (andEL (X = rational_numbers) (Rlt a b) Hc2).
An exact proof term for the current goal is (HneqQ Heq).
Assume Hc3: X = ω ∧ a ∈ b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = ω.
An exact proof term for the current goal is (andEL (X = ω) (a ∈ b) Hc3).
An exact proof term for the current goal is (HneqO Heq).
Assume Hc4: X = ω ∖ {0} ∧ a ∈ b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = ω ∖ {0}.
An exact proof term for the current goal is (andEL (X = ω ∖ {0}) (a ∈ b) Hc4).
An exact proof term for the current goal is (HneqNz Heq).
Assume Hc5: X = 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)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = setprod 2 ω.
An exact proof term for the current goal is (andEL (X = 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 (Hneq2 Heq).
Assume Hc6: X = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = setprod R R.
An exact proof term for the current goal is (andEL (X = 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 (HneqRR Heq).
Assume Hord: ordinal X ∧ X ≠ R ∧ X ≠ rational_numbers ∧ X ≠ setprod 2 ω ∧ X ≠ setprod R R ∧ a ∈ b.
Set T to be the term ((((ordinal X ∧ X ≠ R) ∧ X ≠ rational_numbers) ∧ X ≠ setprod 2 ω) ∧ X ≠ setprod R R).
An exact proof term for the current goal is (andER T (a ∈ b) Hord).
We prove the intermediate claim Hbcmem: b ∈ c.
Apply (Hbc (b ∈ c)) to the current goal.
Assume Hleft6.
Apply (Hleft6 (b ∈ c)) to the current goal.
Assume Hleft5.
Apply (Hleft5 (b ∈ c)) to the current goal.
Assume Hleft4.
Apply (Hleft4 (b ∈ c)) to the current goal.
Assume Hleft3.
Apply (Hleft3 (b ∈ c)) to the current goal.
Assume Hleft2.
Apply (Hleft2 (b ∈ c)) to the current goal.
Assume Hc1: X = R ∧ Rlt b c.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = R.
An exact proof term for the current goal is (andEL (X = R) (Rlt b c) Hc1).
An exact proof term for the current goal is (HneqR Heq).
Assume Hc2: X = rational_numbers ∧ Rlt b c.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = rational_numbers.
An exact proof term for the current goal is (andEL (X = rational_numbers) (Rlt b c) Hc2).
An exact proof term for the current goal is (HneqQ Heq).
Assume Hc3: X = ω ∧ b ∈ c.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = ω.
An exact proof term for the current goal is (andEL (X = ω) (b ∈ c) Hc3).
An exact proof term for the current goal is (HneqO Heq).
Assume Hc4: X = ω ∖ {0} ∧ b ∈ c.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = ω ∖ {0}.
An exact proof term for the current goal is (andEL (X = ω ∖ {0}) (b ∈ c) Hc4).
An exact proof term for the current goal is (HneqNz Heq).
Assume Hc5: X = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ b = (i,m) ∧ c = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = setprod 2 ω.
An exact proof term for the current goal is (andEL (X = setprod 2 ω) (∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ b = (i,m) ∧ c = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) Hc5).
An exact proof term for the current goal is (Hneq2 Heq).
Assume Hc6: X = setprod R R ∧ ∃a1 a2 b1 b2 : set, b = (a1,a2) ∧ c = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = setprod R R.
An exact proof term for the current goal is (andEL (X = setprod R R) (∃a1 a2 b1 b2 : set, b = (a1,a2) ∧ c = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) Hc6).
An exact proof term for the current goal is (HneqRR Heq).
Assume Hord: ordinal X ∧ X ≠ R ∧ X ≠ rational_numbers ∧ X ≠ setprod 2 ω ∧ X ≠ setprod R R ∧ b ∈ c.
Set T to be the term ((((ordinal X ∧ X ≠ R) ∧ X ≠ rational_numbers) ∧ X ≠ setprod 2 ω) ∧ X ≠ setprod R R).
An exact proof term for the current goal is (andER T (b ∈ c) Hord).
We prove the intermediate claim HcOrd: ordinal c.
An exact proof term for the current goal is (ordinal_Hered X HordX c HcX).
We prove the intermediate claim HcTr: TransSet c.
An exact proof term for the current goal is (ordinal_TransSet c HcOrd).
We prove the intermediate claim HbSubc: b ⊆ c.
An exact proof term for the current goal is (HcTr b Hbcmem).
We prove the intermediate claim Hacmem: a ∈ c.
An exact proof term for the current goal is (HbSubc a Habmem).
We will prove (X = R ∧ Rlt a c) ∨ (X = rational_numbers ∧ Rlt a c) ∨ (X = ω ∧ a ∈ c) ∨ (X = ω ∖ {0} ∧ a ∈ c) ∨ (X = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ c = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) ∨ (X = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ c = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) ∨ (ordinal X ∧ X ≠ R ∧ X ≠ rational_numbers ∧ X ≠ setprod 2 ω ∧ X ≠ setprod R R ∧ a ∈ c).
Apply orIR to the current goal.
Apply and6I to the current goal.
An exact proof term for the current goal is HordX.
An exact proof term for the current goal is HneqR.
An exact proof term for the current goal is HneqQ.
An exact proof term for the current goal is Hneq2.
An exact proof term for the current goal is HneqRR.
An exact proof term for the current goal is Hacmem.
∎