Assume H: interval_or_ray_in rational_numbers Q_sqrt2_cut.
We will prove False.
Apply H to the current goal.
Assume Hinterval: ∃a b : set, a ∈ rational_numbers ∧ b ∈ rational_numbers ∧ interval_in rational_numbers a b Q_sqrt2_cut.
Apply Hinterval to the current goal.
Let a be given.
Assume Hexb.
Apply Hexb to the current goal.
Let b be given.
Assume Hab.
We prove the intermediate claim HabQ: a ∈ rational_numbers ∧ b ∈ rational_numbers.
An exact proof term for the current goal is (andEL (a ∈ rational_numbers ∧ b ∈ rational_numbers) (interval_in rational_numbers a b Q_sqrt2_cut) Hab).
We prove the intermediate claim HaQ: a ∈ rational_numbers.
An exact proof term for the current goal is (andEL (a ∈ rational_numbers) (b ∈ rational_numbers) HabQ).
We prove the intermediate claim HbQ: b ∈ rational_numbers.
An exact proof term for the current goal is (andER (a ∈ rational_numbers) (b ∈ rational_numbers) HabQ).
We prove the intermediate claim Hint: interval_in rational_numbers a b Q_sqrt2_cut.
An exact proof term for the current goal is (andER (a ∈ rational_numbers ∧ b ∈ rational_numbers) (interval_in rational_numbers a b Q_sqrt2_cut) Hab).
We prove the intermediate claim H0cut: 0 ∈ Q_sqrt2_cut.
An exact proof term for the current goal is zero_in_Q_sqrt2_cut.
Apply Hint to the current goal.
Assume Hleft3: Q_sqrt2_cut = order_interval rational_numbers a b ∨ Q_sqrt2_cut = halfopen_interval_left_in rational_numbers a b ∨ Q_sqrt2_cut = halfopen_interval_right_in rational_numbers a b.
Apply Hleft3 to the current goal.
Assume Hleft2: Q_sqrt2_cut = order_interval rational_numbers a b ∨ Q_sqrt2_cut = halfopen_interval_left_in rational_numbers a b.
Apply Hleft2 to the current goal.
Assume HeqOI: Q_sqrt2_cut = order_interval rational_numbers a b.
We prove the intermediate claim H0in: 0 ∈ order_interval rational_numbers a b.
rewrite the current goal using HeqOI (from right to left).
An exact proof term for the current goal is H0cut.
We prove the intermediate claim H0pred: order_rel rational_numbers a 0 ∧ order_rel rational_numbers 0 b.
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0 ∧ order_rel rational_numbers x0 b) 0 H0in).
We prove the intermediate claim Ha0: order_rel rational_numbers a 0.
An exact proof term for the current goal is (andEL (order_rel rational_numbers a 0) (order_rel rational_numbers 0 b) H0pred).
We prove the intermediate claim H0b: order_rel rational_numbers 0 b.
An exact proof term for the current goal is (andER (order_rel rational_numbers a 0) (order_rel rational_numbers 0 b) H0pred).
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R a HaQ).
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R b HbQ).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim Halt0: Rlt a 0.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt a 0 Ha0).
We prove the intermediate claim H0blt: Rlt 0 b.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt 0 b H0b).
Set s2 to be the term sqrt_SNo_nonneg 2.
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.
An exact proof term for the current goal is (sqrt_SNo_nonneg_sqr 2 SNo_2 H0le2).
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).
Apply (SNoLt_trichotomy_or_impred b s2 HbS Hs2S False) to the current goal.
Assume Hblts2: b < s2.
We prove the intermediate claim Hbs2: Rlt b s2.
An exact proof term for the current goal is (RltI b s2 HbR Hs2R Hblts2).
Apply (rational_dense_between_reals b s2 HbR Hs2R Hbs2) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume HqProp: Rlt b q ∧ Rlt q s2.
We prove the intermediate claim Hbq: Rlt b q.
An exact proof term for the current goal is (andEL (Rlt b q) (Rlt q s2) HqProp).
We prove the intermediate claim Hqs2: Rlt q s2.
An exact proof term for the current goal is (andER (Rlt b q) (Rlt q s2) HqProp).
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 H0q: Rlt 0 q.
An exact proof term for the current goal is (Rlt_tra 0 b q H0blt Hbq).
We prove the intermediate claim H0ltq: 0 < q.
An exact proof term for the current goal is (RltE_lt 0 q H0q).
We prove the intermediate claim Hqlts2: q < s2.
An exact proof term for the current goal is (RltE_lt q s2 Hqs2).
We prove the intermediate claim Hqqlt2: mul_SNo q q < 2.
We prove the intermediate claim Hqqs2: mul_SNo q q < mul_SNo s2 s2.
An exact proof term for the current goal is (pos_mul_SNo_Lt2 q q s2 s2 HqS HqS Hs2S Hs2S H0ltq H0ltq Hqlts2 Hqlts2).
rewrite the current goal using Hs2sq (from right to left).
An exact proof term for the current goal is Hqqs2.
We prove the intermediate claim HqCut: q ∈ Q_sqrt2_cut.
An exact proof term for the current goal is (SepI rational_numbers (λq0 : set ⇒ mul_SNo q0 q0 < 2) q HqQ Hqqlt2).
We prove the intermediate claim HqInI: q ∈ order_interval rational_numbers a b.
rewrite the current goal using HeqOI (from right to left).
An exact proof term for the current goal is HqCut.
We prove the intermediate claim HqPred: order_rel rational_numbers a q ∧ order_rel rational_numbers q b.
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0 ∧ order_rel rational_numbers x0 b) q HqInI).
We prove the intermediate claim Hqb: order_rel rational_numbers q b.
An exact proof term for the current goal is (andER (order_rel rational_numbers a q) (order_rel rational_numbers q b) HqPred).
We prove the intermediate claim Hqblt: Rlt q b.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt q b Hqb).
An exact proof term for the current goal is ((not_Rlt_sym b q Hbq) Hqblt).
Assume Hbeq: b = s2.
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 Hbeq (from right to left).
An exact proof term for the current goal is HbQ.
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 Hs2ltb: s2 < b.
We prove the intermediate claim Hs2b: Rlt s2 b.
An exact proof term for the current goal is (RltI s2 b Hs2R HbR Hs2ltb).
Apply (rational_dense_between_reals s2 b Hs2R HbR Hs2b) to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqQ: q ∈ rational_numbers.
Assume HqProp: Rlt s2 q ∧ Rlt q b.
We prove the intermediate claim Hs2q: Rlt s2 q.
An exact proof term for the current goal is (andEL (Rlt s2 q) (Rlt q b) HqProp).
We prove the intermediate claim Hqb: Rlt q b.
An exact proof term for the current goal is (andER (Rlt s2 q) (Rlt q b) HqProp).
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 Hs2ltq: s2 < q.
An exact proof term for the current goal is (RltE_lt s2 q Hs2q).
We prove the intermediate claim H0ltq: 0 < q.
An exact proof term for the current goal is (SNoLt_tra 0 s2 q SNo_0 Hs2S HqS H0lts2 Hs2ltq).
We prove the intermediate claim Haq: Rlt a q.
We prove the intermediate claim H0q: Rlt 0 q.
An exact proof term for the current goal is (RltI 0 q real_0 HqR H0ltq).
An exact proof term for the current goal is (Rlt_tra a 0 q Halt0 H0q).
We prove the intermediate claim Haqrel: order_rel rational_numbers a q.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a q Haq).
We prove the intermediate claim Hqbrep: order_rel rational_numbers q b.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q q b Hqb).
We prove the intermediate claim HqInI: q ∈ order_interval rational_numbers a b.
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0 ∧ order_rel rational_numbers x0 b) q HqQ (andI (order_rel rational_numbers a q) (order_rel rational_numbers q b) Haqrel Hqbrep)).
We prove the intermediate claim HqCut: q ∈ Q_sqrt2_cut.
rewrite the current goal using HeqOI (from left to right).
An exact proof term for the current goal is HqInI.
We prove the intermediate claim Hqqlt2: 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 HqCut).
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 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 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 Hqqlt2).
An exact proof term for the current goal is ((SNoLt_irref 2) H2lt2).
Assume HeqHL: Q_sqrt2_cut = halfopen_interval_left_in rational_numbers a b.
We prove the intermediate claim H0in: 0 ∈ halfopen_interval_left_in rational_numbers a b.
rewrite the current goal using HeqHL (from right to left).
An exact proof term for the current goal is H0cut.
We prove the intermediate claim H0pred: (0 = a ∨ order_rel rational_numbers a 0) ∧ order_rel rational_numbers 0 b.
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ (x0 = a ∨ order_rel rational_numbers a x0) ∧ order_rel rational_numbers x0 b) 0 H0in).
We prove the intermediate claim H0ab: 0 = a ∨ order_rel rational_numbers a 0.
An exact proof term for the current goal is (andEL (0 = a ∨ order_rel rational_numbers a 0) (order_rel rational_numbers 0 b) H0pred).
We prove the intermediate claim H0b: order_rel rational_numbers 0 b.
An exact proof term for the current goal is (andER (0 = a ∨ order_rel rational_numbers a 0) (order_rel rational_numbers 0 b) H0pred).
We prove the intermediate claim Hab: order_rel rational_numbers a b.
Apply H0ab to the current goal.
Assume H0eq: 0 = a.
rewrite the current goal using H0eq (from right to left).
An exact proof term for the current goal is H0b.
Assume Ha0: order_rel rational_numbers a 0.
We prove the intermediate claim Halt0: Rlt a 0.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt a 0 Ha0).
We prove the intermediate claim H0blt: Rlt 0 b.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt 0 b H0b).
We prove the intermediate claim Hablt: Rlt a b.
An exact proof term for the current goal is (Rlt_tra a 0 b Halt0 H0blt).
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a b Hablt).
We prove the intermediate claim HainI: a ∈ halfopen_interval_left_in rational_numbers a b.
We prove the intermediate claim Heqaa: a = a.
Use reflexivity.
We prove the intermediate claim Hleft: a = a ∨ order_rel rational_numbers a a.
An exact proof term for the current goal is (orIL (a = a) (order_rel rational_numbers a a) Heqaa).
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ (x0 = a ∨ order_rel rational_numbers a x0) ∧ order_rel rational_numbers x0 b) a HaQ (andI (a = a ∨ order_rel rational_numbers a a) (order_rel rational_numbers a b) Hleft Hab)).
We prove the intermediate claim HainCut: a ∈ Q_sqrt2_cut.
rewrite the current goal using HeqHL (from left to right).
An exact proof term for the current goal is HainI.
Apply (Q_sqrt2_cut_no_min a HainCut) 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 r a) Hrconj).
We prove the intermediate claim Hrlt: Rlt r a.
An exact proof term for the current goal is (andER (r ∈ Q_sqrt2_cut) (Rlt r a) Hrconj).
We prove the intermediate claim HrInI: r ∈ halfopen_interval_left_in rational_numbers a b.
rewrite the current goal using HeqHL (from right to left).
An exact proof term for the current goal is HrCut.
We prove the intermediate claim HrPred: (r = a ∨ order_rel rational_numbers a r) ∧ order_rel rational_numbers r b.
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ (x0 = a ∨ order_rel rational_numbers a x0) ∧ order_rel rational_numbers x0 b) r HrInI).
We prove the intermediate claim HrLeft: r = a ∨ order_rel rational_numbers a r.
An exact proof term for the current goal is (andEL (r = a ∨ order_rel rational_numbers a r) (order_rel rational_numbers r b) HrPred).
Apply HrLeft to the current goal.
Assume Hreq: r = a.
Apply (not_Rlt_refl a (rational_numbers_in_R a HaQ)) to the current goal.
rewrite the current goal using Hreq (from right to left) at position 1.
An exact proof term for the current goal is Hrlt.
Assume Hrel: order_rel rational_numbers a r.
We prove the intermediate claim Halt: Rlt a r.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt a r Hrel).
An exact proof term for the current goal is ((not_Rlt_sym r a Hrlt) Halt).
Assume HeqHR: Q_sqrt2_cut = halfopen_interval_right_in rational_numbers a b.
We prove the intermediate claim H0in: 0 ∈ halfopen_interval_right_in rational_numbers a b.
rewrite the current goal using HeqHR (from right to left).
An exact proof term for the current goal is H0cut.
We prove the intermediate claim H0pred: order_rel rational_numbers a 0 ∧ (0 = b ∨ order_rel rational_numbers 0 b).
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0 ∧ (x0 = b ∨ order_rel rational_numbers x0 b)) 0 H0in).
We prove the intermediate claim Ha0: order_rel rational_numbers a 0.
An exact proof term for the current goal is (andEL (order_rel rational_numbers a 0) (0 = b ∨ order_rel rational_numbers 0 b) H0pred).
We prove the intermediate claim H0b: 0 = b ∨ order_rel rational_numbers 0 b.
An exact proof term for the current goal is (andER (order_rel rational_numbers a 0) (0 = b ∨ order_rel rational_numbers 0 b) H0pred).
We prove the intermediate claim Hab: order_rel rational_numbers a b.
Apply H0b to the current goal.
Assume H0eq: 0 = b.
rewrite the current goal using H0eq (from right to left).
An exact proof term for the current goal is Ha0.
Assume Hrel: order_rel rational_numbers 0 b.
We prove the intermediate claim Halt0: Rlt a 0.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt a 0 Ha0).
We prove the intermediate claim H0blt: Rlt 0 b.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt 0 b Hrel).
We prove the intermediate claim Hablt: Rlt a b.
An exact proof term for the current goal is (Rlt_tra a 0 b Halt0 H0blt).
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a b Hablt).
We prove the intermediate claim HbinI: b ∈ halfopen_interval_right_in rational_numbers a b.
We prove the intermediate claim Heqbb: b = b.
Use reflexivity.
We prove the intermediate claim Hright: b = b ∨ order_rel rational_numbers b b.
An exact proof term for the current goal is (orIL (b = b) (order_rel rational_numbers b b) Heqbb).
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0 ∧ (x0 = b ∨ order_rel rational_numbers x0 b)) b HbQ (andI (order_rel rational_numbers a b) (b = b ∨ order_rel rational_numbers b b) Hab Hright)).
We prove the intermediate claim HbinCut: b ∈ Q_sqrt2_cut.
rewrite the current goal using HeqHR (from left to right).
An exact proof term for the current goal is HbinI.
Apply (Q_sqrt2_cut_no_max b HbinCut) 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 b r) Hrconj).
We prove the intermediate claim HbR: Rlt b r.
An exact proof term for the current goal is (andER (r ∈ Q_sqrt2_cut) (Rlt b r) Hrconj).
We prove the intermediate claim HrInI: r ∈ halfopen_interval_right_in rational_numbers a b.
rewrite the current goal using HeqHR (from right to left).
An exact proof term for the current goal is HrCut.
We prove the intermediate claim HrPred: order_rel rational_numbers a r ∧ (r = b ∨ order_rel rational_numbers r b).
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0 ∧ (x0 = b ∨ order_rel rational_numbers x0 b)) r HrInI).
We prove the intermediate claim HrRight: r = b ∨ order_rel rational_numbers r b.
An exact proof term for the current goal is (andER (order_rel rational_numbers a r) (r = b ∨ order_rel rational_numbers r b) HrPred).
Apply HrRight to the current goal.
Assume Hreq: r = b.
Apply (not_Rlt_refl b (rational_numbers_in_R b HbQ)) to the current goal.
rewrite the current goal using Hreq (from right to left) at position 2.
An exact proof term for the current goal is HbR.
Assume Hrel: order_rel rational_numbers r b.
We prove the intermediate claim Hrltb: Rlt r b.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt r b Hrel).
An exact proof term for the current goal is ((not_Rlt_sym b r HbR) Hrltb).
Assume HeqCI: Q_sqrt2_cut = closed_interval_in rational_numbers a b.
We prove the intermediate claim H0in: 0 ∈ closed_interval_in rational_numbers a b.
rewrite the current goal using HeqCI (from right to left).
An exact proof term for the current goal is H0cut.
We prove the intermediate claim H0pred: (0 = a ∨ order_rel rational_numbers a 0) ∧ (0 = b ∨ order_rel rational_numbers 0 b).
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ (x0 = a ∨ order_rel rational_numbers a x0) ∧ (x0 = b ∨ order_rel rational_numbers x0 b)) 0 H0in).
We prove the intermediate claim H0a: 0 = a ∨ order_rel rational_numbers a 0.
An exact proof term for the current goal is (andEL (0 = a ∨ order_rel rational_numbers a 0) (0 = b ∨ order_rel rational_numbers 0 b) H0pred).
We prove the intermediate claim H0b: 0 = b ∨ order_rel rational_numbers 0 b.
An exact proof term for the current goal is (andER (0 = a ∨ order_rel rational_numbers a 0) (0 = b ∨ order_rel rational_numbers 0 b) H0pred).
We prove the intermediate claim Habdisj: b = a ∨ order_rel rational_numbers a b.
Apply H0a to the current goal.
Assume H0eq: 0 = a.
Apply H0b to the current goal.
Assume H0eqb: 0 = b.
We prove the intermediate claim Hab: b = a.
rewrite the current goal using H0eq (from right to left).
rewrite the current goal using H0eqb (from right to left).
Use reflexivity.
An exact proof term for the current goal is (orIL (b = a) (order_rel rational_numbers a b) Hab).
Assume H0rel: order_rel rational_numbers 0 b.
We prove the intermediate claim H0blt: Rlt 0 b.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt 0 b H0rel).
We prove the intermediate claim Hablt: Rlt a b.
rewrite the current goal using H0eq (from right to left).
An exact proof term for the current goal is H0blt.
We prove the intermediate claim Hab: order_rel rational_numbers a b.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a b Hablt).
An exact proof term for the current goal is (orIR (b = a) (order_rel rational_numbers a b) Hab).
Assume Ha0: order_rel rational_numbers a 0.
We prove the intermediate claim Halt0: Rlt a 0.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt a 0 Ha0).
Apply H0b to the current goal.
Assume H0eqb: 0 = b.
We prove the intermediate claim Hablt: Rlt a b.
rewrite the current goal using H0eqb (from right to left).
An exact proof term for the current goal is Halt0.
We prove the intermediate claim Hab: order_rel rational_numbers a b.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a b Hablt).
An exact proof term for the current goal is (orIR (b = a) (order_rel rational_numbers a b) Hab).
Assume H0rel: order_rel rational_numbers 0 b.
We prove the intermediate claim H0blt: Rlt 0 b.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt 0 b H0rel).
We prove the intermediate claim Hablt: Rlt a b.
An exact proof term for the current goal is (Rlt_tra a 0 b Halt0 H0blt).
We prove the intermediate claim Hab: order_rel rational_numbers a b.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a b Hablt).
An exact proof term for the current goal is (orIR (b = a) (order_rel rational_numbers a b) Hab).
We prove the intermediate claim HbinI: b ∈ closed_interval_in rational_numbers a b.
We prove the intermediate claim Heqbb: b = b.
Use reflexivity.
We prove the intermediate claim Hright: b = b ∨ order_rel rational_numbers b b.
An exact proof term for the current goal is (orIL (b = b) (order_rel rational_numbers b b) Heqbb).
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ (x0 = a ∨ order_rel rational_numbers a x0) ∧ (x0 = b ∨ order_rel rational_numbers x0 b)) b HbQ (andI (b = a ∨ order_rel rational_numbers a b) (b = b ∨ order_rel rational_numbers b b) Habdisj Hright)).
We prove the intermediate claim HbinCut: b ∈ Q_sqrt2_cut.
rewrite the current goal using HeqCI (from left to right).
An exact proof term for the current goal is HbinI.
Apply (Q_sqrt2_cut_no_max b HbinCut) 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 b r) Hrconj).
We prove the intermediate claim HbR: Rlt b r.
An exact proof term for the current goal is (andER (r ∈ Q_sqrt2_cut) (Rlt b r) Hrconj).
We prove the intermediate claim HrInI: r ∈ closed_interval_in rational_numbers a b.
rewrite the current goal using HeqCI (from right to left).
An exact proof term for the current goal is HrCut.
We prove the intermediate claim HrPred: (r = a ∨ order_rel rational_numbers a r) ∧ (r = b ∨ order_rel rational_numbers r b).
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ (x0 = a ∨ order_rel rational_numbers a x0) ∧ (x0 = b ∨ order_rel rational_numbers x0 b)) r HrInI).
We prove the intermediate claim HrRight: r = b ∨ order_rel rational_numbers r b.
An exact proof term for the current goal is (andER (r = a ∨ order_rel rational_numbers a r) (r = b ∨ order_rel rational_numbers r b) HrPred).
Apply HrRight to the current goal.
Assume Hreq: r = b.
Apply (not_Rlt_refl b (rational_numbers_in_R b HbQ)) to the current goal.
rewrite the current goal using Hreq (from right to left) at position 2.
An exact proof term for the current goal is HbR.
Assume Hrel: order_rel rational_numbers r b.
We prove the intermediate claim Hrltb: Rlt r b.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt r b Hrel).
An exact proof term for the current goal is ((not_Rlt_sym b r HbR) Hrltb).
Assume Hray: ∃a : set, a ∈ rational_numbers ∧ ray_in rational_numbers a Q_sqrt2_cut.
Apply Hray to the current goal.
Let a be given.
Assume Hpair.
We prove the intermediate claim HaQ: a ∈ rational_numbers.
An exact proof term for the current goal is (andEL (a ∈ rational_numbers) (ray_in rational_numbers a Q_sqrt2_cut) Hpair).
We prove the intermediate claim Hrayin: ray_in rational_numbers a Q_sqrt2_cut.
An exact proof term for the current goal is (andER (a ∈ rational_numbers) (ray_in rational_numbers a Q_sqrt2_cut) Hpair).
We prove the intermediate claim H0cut: 0 ∈ Q_sqrt2_cut.
An exact proof term for the current goal is zero_in_Q_sqrt2_cut.
We prove the intermediate claim H2Q: 2 ∈ rational_numbers.
An exact proof term for the current goal is two_in_rational_numbers.
We prove the intermediate claim Hm2Q: minus_SNo 2 ∈ rational_numbers.
An exact proof term for the current goal is (rational_minus_SNo 2 H2Q).
We prove the intermediate claim Hm2lt0: minus_SNo 2 < 0.
We will prove minus_SNo 2 < 0.
rewrite the current goal using (minus_SNo_0) (from right to left) at position 2.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 2 SNo_0 SNo_2 SNoLt_0_2).
Apply Hrayin to the current goal.
Assume Hleft: Q_sqrt2_cut = open_ray_upper rational_numbers a ∨ Q_sqrt2_cut = closed_ray_upper rational_numbers a ∨ Q_sqrt2_cut = open_ray_lower rational_numbers a.
Apply Hleft to the current goal.
Assume Hup: Q_sqrt2_cut = open_ray_upper rational_numbers a ∨ Q_sqrt2_cut = closed_ray_upper rational_numbers a.
Apply Hup to the current goal.
Assume HeqU: Q_sqrt2_cut = open_ray_upper rational_numbers a.
We prove the intermediate claim H0in: 0 ∈ open_ray_upper rational_numbers a.
rewrite the current goal using HeqU (from right to left).
An exact proof term for the current goal is H0cut.
We prove the intermediate claim Hrel: order_rel rational_numbers a 0.
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0) 0 H0in).
We prove the intermediate claim Ha0: Rlt a 0.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt a 0 Hrel).
We prove the intermediate claim H02: Rlt 0 2.
An exact proof term for the current goal is (RltI 0 2 real_0 (rational_numbers_in_R 2 H2Q) SNoLt_0_2).
We prove the intermediate claim Ha2: Rlt a 2.
An exact proof term for the current goal is (Rlt_tra a 0 2 Ha0 H02).
We prove the intermediate claim Hrel2: order_rel rational_numbers a 2.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a 2 Ha2).
We prove the intermediate claim H2in: 2 ∈ open_ray_upper rational_numbers a.
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ order_rel rational_numbers a x0) 2 H2Q Hrel2).
We prove the intermediate claim H2cut: 2 ∈ Q_sqrt2_cut.
rewrite the current goal using HeqU (from left to right).
An exact proof term for the current goal is H2in.
An exact proof term for the current goal is (two_not_in_Q_sqrt2_cut H2cut).
Assume HeqU: Q_sqrt2_cut = closed_ray_upper rational_numbers a.
We prove the intermediate claim H0in: 0 ∈ closed_ray_upper rational_numbers a.
rewrite the current goal using HeqU (from right to left).
An exact proof term for the current goal is H0cut.
We prove the intermediate claim Hrel0: 0 = a ∨ order_rel rational_numbers a 0.
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ x0 = a ∨ order_rel rational_numbers a x0) 0 H0in).
Apply Hrel0 to the current goal.
Assume H0eq: 0 = a.
We prove the intermediate claim H02: Rlt 0 2.
An exact proof term for the current goal is (RltI 0 2 real_0 (rational_numbers_in_R 2 H2Q) SNoLt_0_2).
We prove the intermediate claim Ha2: Rlt a 2.
rewrite the current goal using H0eq (from right to left).
An exact proof term for the current goal is H02.
We prove the intermediate claim Hrel2: order_rel rational_numbers a 2.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a 2 Ha2).
We prove the intermediate claim H2in: 2 ∈ closed_ray_upper rational_numbers a.
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ x0 = a ∨ order_rel rational_numbers a x0) 2 H2Q (orIR (2 = a) (order_rel rational_numbers a 2) Hrel2)).
We prove the intermediate claim H2cut: 2 ∈ Q_sqrt2_cut.
rewrite the current goal using HeqU (from left to right).
An exact proof term for the current goal is H2in.
An exact proof term for the current goal is (two_not_in_Q_sqrt2_cut H2cut).
Assume Hrel: order_rel rational_numbers a 0.
We prove the intermediate claim Ha0: Rlt a 0.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt a 0 Hrel).
We prove the intermediate claim H02: Rlt 0 2.
An exact proof term for the current goal is (RltI 0 2 real_0 (rational_numbers_in_R 2 H2Q) SNoLt_0_2).
We prove the intermediate claim Ha2: Rlt a 2.
An exact proof term for the current goal is (Rlt_tra a 0 2 Ha0 H02).
We prove the intermediate claim Hrel2: order_rel rational_numbers a 2.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q a 2 Ha2).
We prove the intermediate claim H2in: 2 ∈ closed_ray_upper rational_numbers a.
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ x0 = a ∨ order_rel rational_numbers a x0) 2 H2Q (orIR (2 = a) (order_rel rational_numbers a 2) Hrel2)).
We prove the intermediate claim H2cut: 2 ∈ Q_sqrt2_cut.
rewrite the current goal using HeqU (from left to right).
An exact proof term for the current goal is H2in.
An exact proof term for the current goal is (two_not_in_Q_sqrt2_cut H2cut).
Assume HeqL: Q_sqrt2_cut = open_ray_lower rational_numbers a.
We prove the intermediate claim H0in: 0 ∈ open_ray_lower rational_numbers a.
rewrite the current goal using HeqL (from right to left).
An exact proof term for the current goal is H0cut.
We prove the intermediate claim Hrel0: order_rel rational_numbers 0 a.
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ order_rel rational_numbers x0 a) 0 H0in).
We prove the intermediate claim H0a: Rlt 0 a.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt 0 a Hrel0).
We prove the intermediate claim Hm20: Rlt (minus_SNo 2) 0.
An exact proof term for the current goal is (RltI (minus_SNo 2) 0 (rational_numbers_in_R (minus_SNo 2) Hm2Q) real_0 Hm2lt0).
We prove the intermediate claim Hm2a: Rlt (minus_SNo 2) a.
An exact proof term for the current goal is (Rlt_tra (minus_SNo 2) 0 a Hm20 H0a).
We prove the intermediate claim Hrelm2: order_rel rational_numbers (minus_SNo 2) a.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q (minus_SNo 2) a Hm2a).
We prove the intermediate claim Hm2in: minus_SNo 2 ∈ open_ray_lower rational_numbers a.
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ order_rel rational_numbers x0 a) (minus_SNo 2) Hm2Q Hrelm2).
We prove the intermediate claim Hm2cut: minus_SNo 2 ∈ Q_sqrt2_cut.
rewrite the current goal using HeqL (from left to right).
An exact proof term for the current goal is Hm2in.
An exact proof term for the current goal is (minus_two_not_in_Q_sqrt2_cut Hm2cut).
Assume HeqL: Q_sqrt2_cut = closed_ray_lower rational_numbers a.
We prove the intermediate claim H0in: 0 ∈ closed_ray_lower rational_numbers a.
rewrite the current goal using HeqL (from right to left).
An exact proof term for the current goal is H0cut.
We prove the intermediate claim Hrel0: 0 = a ∨ order_rel rational_numbers 0 a.
An exact proof term for the current goal is (SepE2 rational_numbers (λx0 : set ⇒ x0 = a ∨ order_rel rational_numbers x0 a) 0 H0in).
Apply Hrel0 to the current goal.
Assume H0eq: 0 = a.
We prove the intermediate claim Hm20: Rlt (minus_SNo 2) 0.
An exact proof term for the current goal is (RltI (minus_SNo 2) 0 (rational_numbers_in_R (minus_SNo 2) Hm2Q) real_0 Hm2lt0).
We prove the intermediate claim Hm2a: Rlt (minus_SNo 2) a.
rewrite the current goal using H0eq (from right to left).
An exact proof term for the current goal is Hm20.
We prove the intermediate claim Hrelm2: order_rel rational_numbers (minus_SNo 2) a.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q (minus_SNo 2) a Hm2a).
We prove the intermediate claim Hm2in: minus_SNo 2 ∈ closed_ray_lower rational_numbers a.
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ x0 = a ∨ order_rel rational_numbers x0 a) (minus_SNo 2) Hm2Q (orIR ((minus_SNo 2) = a) (order_rel rational_numbers (minus_SNo 2) a) Hrelm2)).
We prove the intermediate claim Hm2cut: minus_SNo 2 ∈ Q_sqrt2_cut.
rewrite the current goal using HeqL (from left to right).
An exact proof term for the current goal is Hm2in.
An exact proof term for the current goal is (minus_two_not_in_Q_sqrt2_cut Hm2cut).
Assume Hrel: order_rel rational_numbers 0 a.
We prove the intermediate claim H0a: Rlt 0 a.
An exact proof term for the current goal is (order_rel_Q_implies_Rlt 0 a Hrel).
We prove the intermediate claim Hm20: Rlt (minus_SNo 2) 0.
An exact proof term for the current goal is (RltI (minus_SNo 2) 0 (rational_numbers_in_R (minus_SNo 2) Hm2Q) real_0 Hm2lt0).
We prove the intermediate claim Hm2a: Rlt (minus_SNo 2) a.
An exact proof term for the current goal is (Rlt_tra (minus_SNo 2) 0 a Hm20 H0a).
We prove the intermediate claim Hrelm2: order_rel rational_numbers (minus_SNo 2) a.
An exact proof term for the current goal is (Rlt_implies_order_rel_Q (minus_SNo 2) a Hm2a).
We prove the intermediate claim Hm2in: minus_SNo 2 ∈ closed_ray_lower rational_numbers a.
An exact proof term for the current goal is (SepI rational_numbers (λx0 : set ⇒ x0 = a ∨ order_rel rational_numbers x0 a) (minus_SNo 2) Hm2Q (orIR ((minus_SNo 2) = a) (order_rel rational_numbers (minus_SNo 2) a) Hrelm2)).
We prove the intermediate claim Hm2cut: minus_SNo 2 ∈ Q_sqrt2_cut.
rewrite the current goal using HeqL (from left to right).
An exact proof term for the current goal is Hm2in.
An exact proof term for the current goal is (minus_two_not_in_Q_sqrt2_cut Hm2cut).
∎