Let a and b be given.
Assume HaR HbR Hab.
We will prove ∃q ∈ rational_numbers, Rlt a q ∧ Rlt q b.
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 Hablt: a < b.
An exact proof term for the current goal is (RltE_lt a b Hab).
We prove the intermediate claim HmaR: minus_SNo a ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (real_SNo (minus_SNo a) HmaR).
Set d to be the term add_SNo b (minus_SNo a).
We prove the intermediate claim HdDef: d = add_SNo b (minus_SNo a).
Use reflexivity.
We prove the intermediate claim HdR: d ∈ R.
rewrite the current goal using HdDef (from left to right).
An exact proof term for the current goal is (real_add_SNo b HbR (minus_SNo a) HmaR).
We prove the intermediate claim HdS: SNo d.
An exact proof term for the current goal is (real_SNo d HdR).
We prove the intermediate claim H0ltd: 0 < d.
rewrite the current goal using HdDef (from left to right).
We prove the intermediate claim Hlt: add_SNo a (minus_SNo a) < add_SNo b (minus_SNo a).
An exact proof term for the current goal is (add_SNo_Lt1 a (minus_SNo a) b HaS HmaS HbS Hablt).
We prove the intermediate claim H0eq: add_SNo a (minus_SNo a) = 0.
An exact proof term for the current goal is (add_SNo_minus_SNo_rinv a HaS).
rewrite the current goal using H0eq (from right to left).
An exact proof term for the current goal is Hlt.
Set invd to be the term recip_SNo_pos d.
We prove the intermediate claim HinvdDef: invd = recip_SNo_pos d.
Use reflexivity.
We prove the intermediate claim HinvdR: invd ∈ R.
rewrite the current goal using HinvdDef (from left to right).
An exact proof term for the current goal is (real_recip_SNo_pos d HdR H0ltd).
We prove the intermediate claim HinvdS: SNo invd.
An exact proof term for the current goal is (real_SNo invd HinvdR).
We prove the intermediate claim Hinvdpos: 0 < invd.
An exact proof term for the current goal is (recip_SNo_pos_is_pos d HdS H0ltd).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < d.
Apply (real_E invd HinvdR (∃N ∈ ω, eps_ N < d)) to the current goal.
Assume HinvS: SNo invd.
Assume Hlev.
Assume HinS.
Assume Hlow.
Assume Hup.
Assume Huniq.
Assume Happrox.
We prove the intermediate claim HexNlt: ∃N ∈ ω, mul_SNo (eps_ N) invd < 1.
An exact proof term for the current goal is (SNoS_ordsucc_omega_bdd_eps_pos invd HinS Hinvdpos Hup).
Apply HexNlt to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (mul_SNo (eps_ N) invd < 1) HNpair).
We prove the intermediate claim HmulLt: mul_SNo (eps_ N) invd < 1.
An exact proof term for the current goal is (andER (N ∈ ω) (mul_SNo (eps_ N) invd < 1) HNpair).
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNomega.
We prove the intermediate claim HepsS: SNo (eps_ N).
An exact proof term for the current goal is (SNo_eps_ N HNomega).
We prove the intermediate claim HepsLtDiv: eps_ N < div_SNo 1 invd.
An exact proof term for the current goal is (div_SNo_pos_LtR 1 invd (eps_ N) SNo_1 HinvS HepsS Hinvdpos HmulLt).
We prove the intermediate claim HdivEq: div_SNo 1 invd = d.
We prove the intermediate claim Hposcase: recip_SNo invd = recip_SNo_pos invd.
An exact proof term for the current goal is (recip_SNo_poscase invd Hinvdpos).
We prove the intermediate claim HrecipInv: recip_SNo_pos invd = d.
rewrite the current goal using HinvdDef (from left to right).
An exact proof term for the current goal is (recip_SNo_pos_invol d HdS H0ltd).
We prove the intermediate claim HdivDef: div_SNo 1 invd = mul_SNo 1 (recip_SNo invd).
Use reflexivity.
rewrite the current goal using HdivDef (from left to right).
rewrite the current goal using Hposcase (from left to right).
rewrite the current goal using HrecipInv (from left to right).
An exact proof term for the current goal is (mul_SNo_oneL d HdS).
rewrite the current goal using HdivEq (from right to left).
An exact proof term for the current goal is HepsLtDiv.
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < d) HNpair).
We prove the intermediate claim HepsNlt: eps_ N < d.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < d) HNpair).
We prove the intermediate claim Hexq: ∃q ∈ SNoS_ ω, q < b ∧ b < add_SNo q (eps_ N).
Apply (real_E b HbR (∃q ∈ SNoS_ ω, q < b ∧ b < add_SNo q (eps_ N))) to the current goal.
Assume HbS': SNo b.
Assume Hlev.
Assume HbInS.
Assume Hlow.
Assume Hup.
Assume Huniq.
Assume Happrox.
An exact proof term for the current goal is (Happrox N HNomega).
Apply Hexq to the current goal.
Let q be given.
Assume Hqpair.
Apply Hqpair to the current goal.
Assume HqInS: q ∈ SNoS_ ω.
Assume Hqprop: q < b ∧ b < add_SNo q (eps_ N).
We prove the intermediate claim Hqltb: q < b.
An exact proof term for the current goal is (andEL (q < b) (b < add_SNo q (eps_ N)) Hqprop).
We prove the intermediate claim Hbltqeps: b < add_SNo q (eps_ N).
An exact proof term for the current goal is (andER (q < b) (b < add_SNo q (eps_ N)) Hqprop).
We prove the intermediate claim HqRat: q ∈ rational_numbers.
An exact proof term for the current goal is (Subq_SNoS_omega_rational q HqInS).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R q HqRat).
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 HepsR: eps_ N ∈ R.
An exact proof term for the current goal is (rational_numbers_in_R (eps_ N) (Subq_SNoS_omega_rational (eps_ N) (SNo_eps_SNoS_omega N HNomega))).
We prove the intermediate claim HepsS: SNo (eps_ N).
An exact proof term for the current goal is (real_SNo (eps_ N) HepsR).
We prove the intermediate claim Hbmepsltq: add_SNo b (minus_SNo (eps_ N)) < q.
An exact proof term for the current goal is (add_SNo_minus_Lt1b b (eps_ N) q HbS HepsS HqS Hbltqeps).
We prove the intermediate claim Haepsltb: add_SNo a (eps_ N) < b.
We will prove add_SNo a (eps_ N) < b.
We prove the intermediate claim Hlt1: add_SNo (eps_ N) a < add_SNo d a.
An exact proof term for the current goal is (add_SNo_Lt1 (eps_ N) a d HepsS HaS HdS HepsNlt).
We prove the intermediate claim Hdplus: add_SNo d a = b.
rewrite the current goal using HdDef (from left to right).
An exact proof term for the current goal is (add_SNo_minus_R2' b a HbS HaS).
We prove the intermediate claim Hcom: add_SNo (eps_ N) a = add_SNo a (eps_ N).
An exact proof term for the current goal is (add_SNo_com (eps_ N) a HepsS HaS).
rewrite the current goal using Hcom (from right to left).
rewrite the current goal using Hdplus (from right to left).
An exact proof term for the current goal is Hlt1.
We prove the intermediate claim Haltbmeps: a < add_SNo b (minus_SNo (eps_ N)).
An exact proof term for the current goal is (add_SNo_minus_Lt2b b (eps_ N) a HbS HepsS HaS Haepsltb).
We prove the intermediate claim HbmepsS: SNo (add_SNo b (minus_SNo (eps_ N))).
An exact proof term for the current goal is (SNo_add_SNo b (minus_SNo (eps_ N)) HbS (SNo_minus_SNo (eps_ N) HepsS)).
We prove the intermediate claim Hqlt: a < q.
An exact proof term for the current goal is (SNoLt_tra a (add_SNo b (minus_SNo (eps_ N))) q HaS HbmepsS HqS Haltbmeps Hbmepsltq).
We prove the intermediate claim Haq: Rlt a q.
An exact proof term for the current goal is (RltI a q HaR HqR Hqlt).
We prove the intermediate claim Hqb: Rlt q b.
An exact proof term for the current goal is (RltI q b HqR HbR Hqltb).
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HqRat.
Apply andI to the current goal.
An exact proof term for the current goal is Haq.
An exact proof term for the current goal is Hqb.
∎