theorem RealAnalysis.abs_real_mk_sub_le_aux₁ {a : ℕ → ℚ} {x e : ℝ} {N : ℕ} {ha : IsCauSeq abs a} (h : ∀ (n : ℕ), N ≤ n → |↑(a n) - x| < e) : x - e ≤ Real.mk ⟨a, ha⟩

theorem RealAnalysis.abs_real_mk_sub_le_aux₂ {a : ℕ → ℚ} {x e : ℝ} {N : ℕ} {ha : IsCauSeq abs a} (h : ∀ (n : ℕ), N ≤ n → |↑(a n) - x| < e) : Real.mk ⟨a, ha⟩ ≤ x + e

theorem RealAnalysis.abs_real_mk_sub_le {a : ℕ → ℚ} {x e : ℝ} {ha : IsCauSeq abs a} (h : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → |↑(a n) - x| < e) : |Real.mk ⟨a, ha⟩ - x| ≤ e

theorem RealAnalysis.tendsTo_real_mk {a : ℕ → ℚ} {ha : IsCauSeq abs a} : tendsTo (fun (x : ℕ) => ↑(a x)) (Real.mk ⟨a, ha⟩)