Let d be given.
Assume HdR: d ∈ R.
Assume Hdpos: Rlt 0 d.
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.
An exact proof term for the current goal is (RltE_lt 0 d Hdpos).
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).
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.
∎