Let n be given.

Assume Hn: n ∈ Zplus.

We prove the intermediate claim Hcore: n ∈ ω ∧ n ∉ {0}.

An exact proof term for the current goal is (setminusE ω {0} n Hn).

An exact proof term for the current goal is (andEL (n ∈ ω) (n ∉ {0}) Hcore).

∎