Assume Heq: Q_sqrt2_cut = rational_numbers.
We will prove False.
We prove the intermediate claim H2inQ: 2 ∈ rational_numbers.
An exact proof term for the current goal is two_in_rational_numbers.
We prove the intermediate claim H2inCut: 2 ∈ Q_sqrt2_cut.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is H2inQ.
An exact proof term for the current goal is (two_not_in_Q_sqrt2_cut H2inCut).
∎