Let a and b be given.
Assume Hrel: order_rel rational_numbers a b.
We will prove Rlt a b.
Apply (Hrel (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.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: rational_numbers = R.
An exact proof term for the current goal is (andEL (rational_numbers = R) (Rlt a b) HA).
An exact proof term for the current goal is (rational_numbers_neq_R Heq).
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).
An exact proof term for the current goal is (rational_numbers_neq_omega Heq).
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).
An exact proof term for the current goal is (rational_numbers_neq_omega_nonzero Heq).
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).
An exact proof term for the current goal is (rational_numbers_neq_setprod_2_omega Heq).
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).
An exact proof term for the current goal is (rational_numbers_neq_setprod_R_R 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).
∎