Assume H2: 2 ∈ Q_sqrt2_cut.
We will prove False.
We prove the intermediate claim H2Q: 2 ∈ rational_numbers.
An exact proof term for the current goal is (SepE1 rational_numbers (λq : set ⇒ mul_SNo q q < 2) 2 H2).
We prove the intermediate claim Hlt: mul_SNo 2 2 < 2.
An exact proof term for the current goal is (SepE2 rational_numbers (λq : set ⇒ mul_SNo q q < 2) 2 H2).
We prove the intermediate claim Hpos2: 0 < 2.
An exact proof term for the current goal is SNoLt_0_2.
We prove the intermediate claim H12: 1 < 2.
An exact proof term for the current goal is SNoLt_1_2.
We prove the intermediate claim H1mul: mul_SNo 1 2 < mul_SNo 2 2.
An exact proof term for the current goal is (pos_mul_SNo_Lt' 1 2 2 SNo_1 SNo_2 SNo_2 Hpos2 H12).
We prove the intermediate claim H2lt22: 2 < mul_SNo 2 2.
rewrite the current goal using (mul_SNo_oneL 2 SNo_2) (from right to left) at position 1.
An exact proof term for the current goal is H1mul.
We prove the intermediate claim H2lt2: 2 < 2.
An exact proof term for the current goal is (SNoLt_tra 2 (mul_SNo 2 2) 2 SNo_2 (SNo_mul_SNo 2 2 SNo_2 SNo_2) SNo_2 H2lt22 Hlt).
An exact proof term for the current goal is ((SNoLt_irref 2) H2lt2).
∎