We will prove 0 ∈ Q_sqrt2_cut.

We prove the intermediate claim H0Q: 0 ∈ rational_numbers.

An exact proof term for the current goal is zero_in_rational_numbers.

We prove the intermediate claim H00: mul_SNo 0 0 = 0.

An exact proof term for the current goal is (mul_SNo_zeroL 0 SNo_0).

We prove the intermediate claim Hlt: mul_SNo 0 0 < 2.

rewrite the current goal using H00 (from left to right).

An exact proof term for the current goal is SNoLt_0_2.

An exact proof term for the current goal is (SepI rational_numbers (λq : set ⇒ mul_SNo q q < 2) 0 H0Q Hlt).

∎