We will prove ¬ countable (closed_interval 0 1).
Assume Hcount: countable (closed_interval 0 1).
We will prove False.
We prove the intermediate claim HRcount: atleastp R ω.
An exact proof term for the current goal is (atleastp_tra R (closed_interval 0 1) ω atleastp_R_closed_interval_0_1 Hcount).
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 HRcount.
An exact proof term for the current goal is (form100_22_real_uncountable_atleastp Hcount_real).
∎