Let X, a and b be given.
Assume Hwo: well_ordered_set X.
Assume Hab: a ∈ b.
We will prove order_rel X a b.
Set T0 to be the term ordinal X ∧ X ≠ R.
Set T1 to be the term T0 ∧ X ≠ rational_numbers.
Set T2 to be the term T1 ∧ X ≠ setprod 2 ω.
Set T3 to be the term T2 ∧ X ≠ setprod R R.
We prove the intermediate claim HT3: T3.
An exact proof term for the current goal is Hwo.
We prove the intermediate claim HT2: T2.
An exact proof term for the current goal is (andEL T2 (X ≠ setprod R R) HT3).
We prove the intermediate claim HneqRR: X ≠ setprod R R.
An exact proof term for the current goal is (andER T2 (X ≠ setprod R R) HT3).
We prove the intermediate claim HT1: T1.
An exact proof term for the current goal is (andEL T1 (X ≠ setprod 2 ω) HT2).
We prove the intermediate claim Hneq2omega: X ≠ setprod 2 ω.
An exact proof term for the current goal is (andER T1 (X ≠ setprod 2 ω) HT2).
We prove the intermediate claim HT0: T0.
An exact proof term for the current goal is (andEL T0 (X ≠ rational_numbers) HT1).
We prove the intermediate claim HneqRat: X ≠ rational_numbers.
An exact proof term for the current goal is (andER T0 (X ≠ rational_numbers) HT1).
We prove the intermediate claim Hord: ordinal X.
An exact proof term for the current goal is (andEL (ordinal X) (X ≠ R) HT0).
We prove the intermediate claim HneqR: X ≠ R.
An exact proof term for the current goal is (andER (ordinal X) (X ≠ R) HT0).
We will prove (X = R ∧ Rlt a b) ∨ (X = rational_numbers ∧ Rlt a b) ∨ (X = ω ∧ a ∈ b) ∨ (X = ω ∖ {0} ∧ a ∈ b) ∨ (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)))) ∨ (X = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (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 ∈ b).
Apply orIR to the current goal.
We will prove ordinal X ∧ X ≠ R ∧ X ≠ rational_numbers ∧ X ≠ setprod 2 ω ∧ X ≠ setprod R R ∧ a ∈ b.
Set T0' to be the term ordinal X ∧ X ≠ R.
Set T1' to be the term T0' ∧ X ≠ rational_numbers.
Set T2' to be the term T1' ∧ X ≠ setprod 2 ω.
Set T3' to be the term T2' ∧ X ≠ setprod R R.
Apply andI to the current goal.
We will prove T3'.
Apply andI to the current goal.
We will prove T2'.
Apply andI to the current goal.
We will prove T1'.
Apply andI to the current goal.
We will prove T0'.
Apply andI to the current goal.
An exact proof term for the current goal is Hord.
An exact proof term for the current goal is HneqR.
An exact proof term for the current goal is HneqRat.
An exact proof term for the current goal is Hneq2omega.
An exact proof term for the current goal is HneqRR.
An exact proof term for the current goal is Hab.
∎