proposition: Lemma lim_const_min_1_over_n_plus_1 : ∀ x : ℝ, Un_cv (fun (n : ℕ) ↦ x - 1 / (INR n + 1)) x.
proof: Proof. Take x : ℝ. It holds that (x = x - 0) (i). rewrite (i) at 1. apply CV_minus with (An := fun (n : ℕ) ↦ x) (Bn := fun (n : ℕ) ↦ 1 / (INR n + 1)) (l1 := x) (l2 := 0). - We need to show that ((constant_sequence x) ⟶ x). By lim_const_seq we conclude that ((constant_sequence x) ⟶ x). - We need to show that (Un_cv d 0). By lim_d_0 we conclude that (Un_cv d 0). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type Automation Libs.Analysis.Sequences Libs.Analysis.Subsequences Libs.Analysis.SupAndInf Libs.Analysis.SequentialAccumulationPoints Notations Tactics