Let q be given.
Assume Hq: q ∈ Q_sqrt2_cut.
We will prove ∃r : set, r ∈ Q_sqrt2_cut ∧ Rlt r q.
We prove the intermediate claim HnegqCut: minus_SNo q ∈ Q_sqrt2_cut.
An exact proof term for the current goal is (Q_sqrt2_cut_neg_closed q Hq).
Apply (Q_sqrt2_cut_no_max (minus_SNo q) HnegqCut) to the current goal.
Let r be given.
Assume Hrconj.
We prove the intermediate claim HrCut: r ∈ Q_sqrt2_cut.
An exact proof term for the current goal is (andEL (r ∈ Q_sqrt2_cut) (Rlt (minus_SNo q) r) Hrconj).
We prove the intermediate claim Hlt: Rlt (minus_SNo q) r.
An exact proof term for the current goal is (andER (r ∈ Q_sqrt2_cut) (Rlt (minus_SNo q) r) Hrconj).
Set s to be the term minus_SNo r.
We prove the intermediate claim HsCut: s ∈ Q_sqrt2_cut.
An exact proof term for the current goal is (Q_sqrt2_cut_neg_closed r HrCut).
We prove the intermediate claim HrQ: r ∈ rational_numbers.
An exact proof term for the current goal is (SepE1 rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) r HrCut).
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 HrR: r ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R r HrQ).
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 HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HnegqR: minus_SNo q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R (minus_SNo q) (SepE1 rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) (minus_SNo q) HnegqCut)).
We prove the intermediate claim HnegqS: SNo (minus_SNo q).
An exact proof term for the current goal is (real_SNo (minus_SNo q) HnegqR).
We prove the intermediate claim HltS: minus_SNo q < r.
An exact proof term for the current goal is (RltE_lt (minus_SNo q) r Hlt).
We prove the intermediate claim Hneglt: minus_SNo r < minus_SNo (minus_SNo q).
An exact proof term for the current goal is (minus_SNo_Lt_contra (minus_SNo q) r HnegqS HrS HltS).
We prove the intermediate claim Hslt: s < q.
We prove the intermediate claim Hinv: minus_SNo (minus_SNo q) = q.
An exact proof term for the current goal is (minus_SNo_invol q (real_SNo q HqR)).
rewrite the current goal using Hinv (from right to left).
An exact proof term for the current goal is Hneglt.
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R s (SepE1 rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) s HsCut)).
We prove the intermediate claim Hsq: Rlt s q.
An exact proof term for the current goal is (RltI s q HsR HqR Hslt).
We use s to witness the existential quantifier.
An exact proof term for the current goal is (andI (s ∈ Q_sqrt2_cut) (Rlt s q) HsCut Hsq).
∎