Let q be given.
Assume Hq: q ∈ Q_sqrt2_cut.
We will prove ∃r : set, r ∈ Q_sqrt2_cut ∧ Rlt q r.
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 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 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).
Apply (SNoLt_trichotomy_or_impred q 0 HqS SNo_0 (∃r : set, r ∈ Q_sqrt2_cut ∧ Rlt q r)) to the current goal.
Assume Hqlt0: q < 0.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is zero_in_Q_sqrt2_cut.
An exact proof term for the current goal is (RltI q 0 HqR real_0 Hqlt0).
Assume Hqeq0: q = 0.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim H1Q: 1 ∈ rational_numbers.
An exact proof term for the current goal is one_in_rational_numbers.
We prove the intermediate claim H11: mul_SNo 1 1 < 2.
We will prove mul_SNo 1 1 < 2.
rewrite the current goal using (mul_SNo_oneL 1 SNo_1) (from left to right).
An exact proof term for the current goal is SNoLt_1_2.
An exact proof term for the current goal is (SepI rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) 1 H1Q H11).
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R 1 one_in_rational_numbers).
rewrite the current goal using Hqeq0 (from left to right).
An exact proof term for the current goal is (RltI 0 1 real_0 H1R SNoLt_0_1).
Assume H0ltq: 0 < q.
Set s2 to be the term sqrt_SNo_nonneg 2.
We prove the intermediate claim Hs2Def: s2 = sqrt_SNo_nonneg 2.
Use reflexivity.
We prove the intermediate claim H2R: 2 ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R 2 two_in_rational_numbers).
We prove the intermediate claim H0le2: 0 ≤ 2.
An exact proof term for the current goal is (SNoLtLe 0 2 SNoLt_0_2).
We prove the intermediate claim Hs2R: s2 ∈ R.
An exact proof term for the current goal is (sqrt_SNo_nonneg_real 2 H2R H0le2).
We prove the intermediate claim Hs2S: SNo s2.
An exact proof term for the current goal is (real_SNo s2 Hs2R).
We prove the intermediate claim Hs2nonneg: 0 ≤ s2.
An exact proof term for the current goal is (sqrt_SNo_nonneg_nonneg 2 SNo_2 H0le2).
We prove the intermediate claim Hs2sq: mul_SNo s2 s2 = 2.
We will prove mul_SNo s2 s2 = 2.
rewrite the current goal using Hs2Def (from left to right) at position 1.
rewrite the current goal using Hs2Def (from left to right) at position 2.
An exact proof term for the current goal is (sqrt_SNo_nonneg_sqr 2 SNo_2 H0le2).
We prove the intermediate claim Hqlts2: q < s2.
Apply (SNoLt_trichotomy_or_impred q s2 HqS Hs2S (q < s2)) to the current goal.
Assume Hlt: q < s2.
An exact proof term for the current goal is Hlt.
Assume Heq: q = s2.
Apply FalseE to the current goal.
We prove the intermediate claim Hirr: s2 ∈ real ∖ rational.
An exact proof term for the current goal is sqrt_2_irrational.
We prove the intermediate claim Hnotrat: s2 ∉ rational.
An exact proof term for the current goal is (setminusE2 real rational s2 Hirr).
We prove the intermediate claim Hs2Q: s2 ∈ rational_numbers.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HqQ.
We prove the intermediate claim HdefQ: rational_numbers = rational.
Use reflexivity.
We prove the intermediate claim Hs2rat: s2 ∈ rational.
rewrite the current goal using HdefQ (from right to left).
An exact proof term for the current goal is Hs2Q.
An exact proof term for the current goal is (Hnotrat Hs2rat).
Assume Hs2ltq: s2 < q.
Apply FalseE to the current goal.
We prove the intermediate claim Hs2neq0: s2 ≠ 0.
Assume Hs2eq0: s2 = 0.
Apply neq_2_0 to the current goal.
rewrite the current goal using Hs2sq (from right to left).
rewrite the current goal using Hs2eq0 (from left to right).
rewrite the current goal using (mul_SNo_zeroL 0 SNo_0) (from left to right).
Use reflexivity.
We prove the intermediate claim H0lts2: 0 < s2.
We prove the intermediate claim Hdisj: 0 < s2 ∨ 0 = s2.
An exact proof term for the current goal is (SNoLeE 0 s2 SNo_0 Hs2S Hs2nonneg).
Apply Hdisj to the current goal.
Assume Hlt0: 0 < s2.
An exact proof term for the current goal is Hlt0.
Assume Heq0: 0 = s2.
Apply FalseE to the current goal.
We prove the intermediate claim Hs2eq0: s2 = 0.
rewrite the current goal using Heq0 (from right to left).
Use reflexivity.
An exact proof term for the current goal is (Hs2neq0 Hs2eq0).
We prove the intermediate claim HqqS: SNo (mul_SNo q q).
An exact proof term for the current goal is (SNo_mul_SNo q q HqS HqS).
We prove the intermediate claim Hs2s2S: SNo (mul_SNo s2 s2).
An exact proof term for the current goal is (SNo_mul_SNo s2 s2 Hs2S Hs2S).
We prove the intermediate claim Hs2s2ltqq: mul_SNo s2 s2 < mul_SNo q q.
An exact proof term for the current goal is (pos_mul_SNo_Lt2 s2 s2 q q Hs2S Hs2S HqS HqS H0lts2 H0lts2 Hs2ltq Hs2ltq).
We prove the intermediate claim H2ltqq: 2 < mul_SNo q q.
rewrite the current goal using Hs2sq (from right to left) at position 1.
An exact proof term for the current goal is Hs2s2ltqq.
We prove the intermediate claim H2lt2: 2 < 2.
An exact proof term for the current goal is (SNoLt_tra 2 (mul_SNo q q) 2 SNo_2 HqqS SNo_2 H2ltqq Hqq).
An exact proof term for the current goal is ((SNoLt_irref 2) H2lt2).
We prove the intermediate claim Hqs2: Rlt q s2.
An exact proof term for the current goal is (RltI q s2 HqR Hs2R Hqlts2).
Apply (rational_dense_between_reals q s2 HqR Hs2R Hqs2) to the current goal.
Let r be given.
Assume Hrpair.
Apply Hrpair to the current goal.
Assume HrQ: r ∈ rational_numbers.
Assume Hrlt: Rlt q r ∧ Rlt r s2.
We prove the intermediate claim Hqr: Rlt q r.
An exact proof term for the current goal is (andEL (Rlt q r) (Rlt r s2) Hrlt).
We prove the intermediate claim Hrs2: Rlt r s2.
An exact proof term for the current goal is (andER (Rlt q r) (Rlt r s2) Hrlt).
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 HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim Hqrrlt: q < r.
An exact proof term for the current goal is (RltE_lt q r Hqr).
We prove the intermediate claim Hrs2lt: r < s2.
An exact proof term for the current goal is (RltE_lt r s2 Hrs2).
We prove the intermediate claim H0ltr: 0 < r.
An exact proof term for the current goal is (SNoLt_tra 0 q r SNo_0 HqS HrS H0ltq Hqrrlt).
We prove the intermediate claim Hrrlt2: mul_SNo r r < 2.
We will prove mul_SNo r r < 2.
We prove the intermediate claim Hrrlts2: mul_SNo r r < mul_SNo s2 s2.
An exact proof term for the current goal is (pos_mul_SNo_Lt2 r r s2 s2 HrS HrS Hs2S Hs2S H0ltr H0ltr Hrs2lt Hrs2lt).
rewrite the current goal using Hs2sq (from right to left).
An exact proof term for the current goal is Hrrlts2.
We prove the intermediate claim HrCut: r ∈ Q_sqrt2_cut.
An exact proof term for the current goal is (SepI rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) r HrQ Hrrlt2).
We use r to witness the existential quantifier.
An exact proof term for the current goal is (andI (r ∈ Q_sqrt2_cut) (Rlt q r) HrCut Hqr).
∎