We will prove False.

We prove the intermediate claim Hequip: equip ω rational_numbers.

We prove the intermediate claim HdefQ: rational_numbers = rational.

Use reflexivity.

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

An exact proof term for the current goal is form100_3.

We prove the intermediate claim Hequip_sym: equip rational_numbers ω.

An exact proof term for the current goal is (equip_sym ω rational_numbers Hequip).

We prove the intermediate claim Hcount_Q: atleastp rational_numbers ω.

An exact proof term for the current goal is (equip_atleastp rational_numbers ω Hequip_sym).

We prove the intermediate claim Hcount_prod: atleastp (setprod R R) ω.

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

An exact proof term for the current goal is Hcount_Q.

We prove the intermediate claim Hinj_R_prod: atleastp R (setprod R R).

We will prove ∃f : set → set, inj R (setprod R R) f.

We use (λx : set ⇒ (x,0)) to witness the existential quantifier.

Apply (injI R (setprod R R) (λx : set ⇒ (x,0))) to the current goal.

Let x be given.

Assume Hx: x ∈ R.

We will prove (x,0) ∈ setprod R R.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x 0 Hx real_0).

Let x be given.

Assume Hx: x ∈ R.

Let z be given.

Assume Hz: z ∈ R.

Assume Hxz: (x,0) = (z,0).

We will prove x = z.

We prove the intermediate claim Hcoords: x = z ∧ 0 = 0.

An exact proof term for the current goal is (tuple_eq_coords x 0 z 0 Hxz).

An exact proof term for the current goal is (andEL (x = z) (0 = 0) Hcoords).

We prove the intermediate claim Hcount_R: atleastp R ω.

An exact proof term for the current goal is (atleastp_tra R (setprod R R) ω Hinj_R_prod Hcount_prod).

We prove the intermediate claim HdefR: R = real.

Use reflexivity.

We prove the intermediate claim Hcount_real: atleastp real ω.

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

An exact proof term for the current goal is Hcount_R.

An exact proof term for the current goal is (form100_22_real_uncountable_atleastp Hcount_real).

∎