Assume Heq: rational_numbers = ω.
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 Hm1omega: minus_SNo 1 ∈ ω.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hm1Q.
An exact proof term for the current goal is (minus_one_not_in_omega Hm1omega).
∎