Let a and b be given.
Assume Hab: order_rel ω a b.
We will prove a ∈ b.
We prove the intermediate claim HnotTrSing1: ¬ TransSet {1}.
Assume Htr: TransSet {1}.
We will prove False.
We prove the intermediate claim H1in: 1 ∈ {1}.
An exact proof term for the current goal is (SingI 1).
We prove the intermediate claim Hsub: 1 ⊆ {1}.
An exact proof term for the current goal is (Htr 1 H1in).
We prove the intermediate claim H0in1: 0 ∈ 1.
An exact proof term for the current goal is In_0_1.
We prove the intermediate claim H0inSing1: 0 ∈ {1}.
An exact proof term for the current goal is (Hsub 0 H0in1).
We prove the intermediate claim Heq: 0 = 1.
An exact proof term for the current goal is (SingE 1 0 H0inSing1).
An exact proof term for the current goal is (neq_0_1 Heq).
We prove the intermediate claim HnotSing1omega: {1} ∉ ω.
Assume H: {1} ∈ ω.
We will prove False.
We prove the intermediate claim Hnat: nat_p {1}.
An exact proof term for the current goal is (omega_nat_p {1} H).
We prove the intermediate claim Hord: ordinal {1}.
An exact proof term for the current goal is (nat_p_ordinal {1} Hnat).
We prove the intermediate claim Htr: TransSet {1}.
An exact proof term for the current goal is (ordinal_TransSet {1} Hord).
An exact proof term for the current goal is (HnotTrSing1 Htr).
Apply Hab to the current goal.
Assume Hleft.
Apply Hleft to the current goal.
Assume Hleft2.
Apply Hleft2 to the current goal.
Assume Hleft3.
Apply Hleft3 to the current goal.
Assume Hleft4.
Apply Hleft4 to the current goal.
Assume H12.
Apply H12 to the current goal.
Assume H1: ω = R ∧ Rlt a b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: ω = R.
An exact proof term for the current goal is (andEL (ω = R) (Rlt a b) H1).
We prove the intermediate claim HeqR: R = ω.
Use symmetry.
An exact proof term for the current goal is Heq.
An exact proof term for the current goal is (R_neq_omega HeqR).
Assume H2: ω = rational_numbers ∧ Rlt 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) (Rlt a b) H2).
We prove the intermediate claim Hm1Q: minus_SNo 1 ∈ rational_numbers.
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 left to right).
An exact proof term for the current goal is Hm1rat.
We prove the intermediate claim Hm1omega: minus_SNo 1 ∈ ω.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hm1Q.
We prove the intermediate claim Hle0: 0 ≤ minus_SNo 1.
An exact proof term for the current goal is (omega_nonneg (minus_SNo 1) Hm1omega).
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).
Assume H3: ω = ω ∧ a ∈ b.
An exact proof term for the current goal is (andER (ω = ω) (a ∈ b) H3).
Assume H4: ω = ω ∖ {0} ∧ a ∈ b.
An exact proof term for the current goal is (andER (ω = ω ∖ {0}) (a ∈ b) H4).
Assume H5: ω = 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 2 ω.
An exact proof term for the current goal is (andEL (ω = 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))) H5).
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 HpOmega: (0,1) ∈ ω.
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 HSingOmega: {1} ∈ ω.
rewrite the current goal using tuple_0_1_eq_Sing1 (from right to left).
An exact proof term for the current goal is HpOmega.
An exact proof term for the current goal is (HnotSing1omega HSingOmega).
Assume H6: ω = 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 R R.
An exact proof term for the current goal is (andEL (ω = setprod R R) (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) H6).
We prove the intermediate claim HpRR: (0,1) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R 0 1 real_0 real_1).
We prove the intermediate claim HpOmega: (0,1) ∈ ω.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HpRR.
We prove the intermediate claim HSingOmega: {1} ∈ ω.
rewrite the current goal using tuple_0_1_eq_Sing1 (from right to left).
An exact proof term for the current goal is HpOmega.
An exact proof term for the current goal is (HnotSing1omega HSingOmega).
Assume H7: ordinal ω ∧ ω ≠ R ∧ ω ≠ rational_numbers ∧ ω ≠ setprod 2 ω ∧ ω ≠ setprod R R ∧ a ∈ b.
Set T to be the term ((((ordinal ω ∧ ω ≠ R) ∧ ω ≠ rational_numbers) ∧ ω ≠ setprod 2 ω) ∧ ω ≠ setprod R R).
An exact proof term for the current goal is (andER T (a ∈ b) H7).
∎