Let q be given.
Assume Hq: q ∈ Q_sqrt2_cut.
We will prove minus_SNo q ∈ Q_sqrt2_cut.
We prove the intermediate claim HqQ: q ∈ rational_numbers.
An exact proof term for the current goal is (SepE1 rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) q Hq).
We prove the intermediate claim Hqq: mul_SNo q q < 2.
An exact proof term for the current goal is (SepE2 rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) q Hq).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqQ).
We prove the intermediate claim HqS: SNo q.
An exact proof term for the current goal is (real_SNo q HqR).
We prove the intermediate claim HnegQ: minus_SNo q ∈ rational_numbers.
An exact proof term for the current goal is (rational_minus_SNo q HqQ).
We prove the intermediate claim HnegR: minus_SNo q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R (minus_SNo q) HnegQ).
We prove the intermediate claim HnegS: SNo (minus_SNo q).
An exact proof term for the current goal is (real_SNo (minus_SNo q) HnegR).
We prove the intermediate claim Hnegneg: mul_SNo (minus_SNo q) (minus_SNo q) < 2.
We will prove mul_SNo (minus_SNo q) (minus_SNo q) < 2.
rewrite the current goal using (mul_SNo_minus_minus q q HqS HqS) (from left to right).
An exact proof term for the current goal is Hqq.
An exact proof term for the current goal is (SepI rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) (minus_SNo q) HnegQ Hnegneg).
∎