Assume Heq: setprod R R = (ω ∖ {0}).
We will prove False.
We prove the intermediate claim HpRR: (0,1) ∈ setprod R R.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R 0 1 real_0 real_1).
We prove the intermediate claim HpNZ: (0,1) ∈ (ω ∖ {0}).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HpRR.
We prove the intermediate claim Hcore: (0,1) ∈ ω ∧ (0,1) ∉ {0}.
An exact proof term for the current goal is (setminusE ω {0} (0,1) HpNZ).
We prove the intermediate claim HpOmega: (0,1) ∈ ω.
An exact proof term for the current goal is (andEL ((0,1) ∈ ω) ((0,1) ∉ {0}) Hcore).
We prove the intermediate claim HSingOmega: {1} ∈ ω.
rewrite the current goal using tuple_0_1_eq_Sing1 (from right to left).
An exact proof term for the current goal is HpOmega.
An exact proof term for the current goal is (Sing1_not_in_omega HSingOmega).
∎