Assume Heq: R = ω ∖ {0}.
We will prove False.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
We prove the intermediate claim Heq': real = ω ∖ {0}.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim Hsub: (ω ∖ {0}) ⊆ ω.
An exact proof term for the current goal is (setminus_Subq ω {0}).
We prove the intermediate claim Hcount_nonzero: atleastp (ω ∖ {0}) ω.
An exact proof term for the current goal is (Subq_atleastp (ω ∖ {0}) ω Hsub).
We prove the intermediate claim Hreal_countable: atleastp real ω.
rewrite the current goal using Heq' (from left to right) at position 1.
An exact proof term for the current goal is Hcount_nonzero.
An exact proof term for the current goal is (form100_22_real_uncountable_atleastp Hreal_countable).
∎