Assume Heq: Zplus = ω.

We will prove False.

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 H0Z: 0 ∈ Zplus.

rewrite the current goal using Heq (from left to right).

An exact proof term for the current goal is H0omega.

An exact proof term for the current goal is (zero_not_in_Zplus H0Z).

∎