We will prove 1 ∈ ω ∖ {0}.

We prove the intermediate claim H1omega: 1 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 1 nat_1).

We prove the intermediate claim H1not0: 1 ∉ {0}.

Assume H1: 1 ∈ {0}.

We will prove False.

We prove the intermediate claim Heq: 1 = 0.

An exact proof term for the current goal is (SingE 0 1 H1).

An exact proof term for the current goal is (neq_1_0 Heq).

An exact proof term for the current goal is (setminusI ω {0} 1 H1omega H1not0).

∎