Let n be given.

Assume HnNat HnNeq.

We will prove n ∈ ω ∖ {0}.

We prove the intermediate claim HnOmega: n ∈ ω.

An exact proof term for the current goal is (nat_p_omega n HnNat).

We prove the intermediate claim Hnnot0: n ∉ {0}.

Assume Hn0: n ∈ {0}.

We will prove False.

We prove the intermediate claim Heq: n = 0.

An exact proof term for the current goal is (SingE 0 n Hn0).

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

An exact proof term for the current goal is (setminusI ω {0} n HnOmega Hnnot0).

∎