Assume Heq: ω ∖ {0} = ω.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim H0nonz: 0 ∈ (ω ∖ {0}).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is H0omega.
We prove the intermediate claim Hnot0: 0 ∉ {0}.
An exact proof term for the current goal is (setminusE2 ω {0} 0 H0nonz).
An exact proof term for the current goal is (Hnot0 (SingI 0)).
∎