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: R = R ∧ Rlt a b.

An exact proof term for the current goal is (andER (R = R) (Rlt a b) HA).

Assume HB: R = rational_numbers ∧ Rlt a b.

Apply FalseE to the current goal.

We prove the intermediate claim Heq: R = rational_numbers.

An exact proof term for the current goal is (andEL (R = rational_numbers) (Rlt a b) HB).

An exact proof term for the current goal is (R_neq_rational_numbers Heq).

Assume HC: R = ω ∧ 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 = ω) (a ∈ b) HC).

An exact proof term for the current goal is (R_neq_omega Heq).

Assume HD: R = ω ∖ {0} ∧ a ∈ b.

Apply FalseE to the current goal.

We prove the intermediate claim Heq: R = ω ∖ {0}.

An exact proof term for the current goal is (andEL (R = ω ∖ {0}) (a ∈ b) HD).

An exact proof term for the current goal is (R_neq_omega_nonzero Heq).

Assume HE: 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: R = setprod 2 ω.

An exact proof term for the current goal is (andEL (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))) HE).

An exact proof term for the current goal is (R_neq_setprod_2_omega Heq).

Assume HF: R = 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: R = setprod R R.

An exact proof term for the current goal is (andEL (R = setprod R R) (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) HF).

Apply setprod_R_R_neq_R to the current goal.

rewrite the current goal using Heq (from right to left).

Use reflexivity.

Assume Hord: ordinal R ∧ R ≠ R ∧ R ≠ rational_numbers ∧ R ≠ setprod 2 ω ∧ 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 HneqRRset.

Apply Hcore2 to the current goal.

Assume Hcore3 Hneq2omega.

Apply Hcore3 to the current goal.

Assume Hcore4 HneqRat.

Apply Hcore4 to the current goal.

Assume HordR HneqRR.

We prove the intermediate claim Hrefl: R = R.

Use reflexivity.

An exact proof term for the current goal is (HneqRR Hrefl).