Assume Heq: rational_numbers = ω ∖ {0}.
We will prove False.
We prove the intermediate claim Hm1Q: minus_SNo 1 ∈ rational_numbers.
An exact proof term for the current goal is minus_one_in_rational_numbers.
We prove the intermediate claim Hm1NZ: minus_SNo 1 ∈ ω ∖ {0}.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hm1Q.
We prove the intermediate claim Hm1omega: minus_SNo 1 ∈ ω.
An exact proof term for the current goal is (setminusE1 ω {0} (minus_SNo 1) Hm1NZ).
An exact proof term for the current goal is (minus_one_not_in_omega Hm1omega).
∎