Let n be given.
Assume Hn: n ∈ Zplus.
We prove the intermediate claim HnOmega: n ∈ ω.
An exact proof term for the current goal is (Zplus_mem_omega n Hn).
We prove the intermediate claim HsuccOmega: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnOmega).
We prove the intermediate claim HsuccNot0: ordsucc n ∉ {0}.
Assume H0: ordsucc n ∈ {0}.
We will prove False.
We prove the intermediate claim Heq0: ordsucc n = 0.
An exact proof term for the current goal is (SingE 0 (ordsucc n) H0).
An exact proof term for the current goal is (neq_ordsucc_0 n Heq0).
An exact proof term for the current goal is (setminusI ω {0} (ordsucc n) HsuccOmega HsuccNot0).
∎