proposition: Lemma lim_d_0 : Un_cv d 0.
proof: Proof. We need to show that (Un_cv (fun n => 1 / (n + 1)) 0). We need to show that (for all eps : ℝ, eps > 0 ⇨ there exists N : ℕ, for all n : ℕ, (n ≥ N)%nat ⇨ ｜ 1 / (n + 1) - 0 ｜ < eps ). Take ε : ℝ; such that (ε > 0). By archimed_mod it holds that (there exists n : ℕ, n > / ε). Obtain such an n1. Choose N := n1. Take n : ℕ; such that (n ≥ n1)%nat. It suffices to show that (-ε < 1 / (n + 1) - 0 < ε). We show both (-ε < 1 / (n + 1) - 0) and (1 / (n + 1) - 0 < ε). - It holds that (0 < n + 1). We conclude that (& -ε < 0 < / (n + 1) = 1 / (n + 1) - 0). - We claim that (/ ε < n + 1). { We conclude that (& / ε < n1 <= n <= n + 1). } We conclude that (& 1 / (n + 1) - 0 = / (n + 1) < / / ε = ε). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations