Assume Hm2: minus_SNo 2 ∈ Q_sqrt2_cut.
We will prove False.
We prove the intermediate claim Hm2lt: mul_SNo (minus_SNo 2) (minus_SNo 2) < 2.
An exact proof term for the current goal is (SepE2 rational_numbers (λq : set ⇒ mul_SNo q q < 2) (minus_SNo 2) Hm2).
We prove the intermediate claim H22lt: mul_SNo 2 2 < 2.
We will prove mul_SNo 2 2 < 2.
rewrite the current goal using (mul_SNo_minus_minus 2 2 SNo_2 SNo_2) (from right to left) at position 1.
An exact proof term for the current goal is Hm2lt.
We prove the intermediate claim H2Q: 2 ∈ rational_numbers.
An exact proof term for the current goal is two_in_rational_numbers.
We prove the intermediate claim H2cut: 2 ∈ Q_sqrt2_cut.
An exact proof term for the current goal is (SepI rational_numbers (λq : set ⇒ mul_SNo q q < 2) 2 H2Q H22lt).
An exact proof term for the current goal is (two_not_in_Q_sqrt2_cut H2cut).
∎