proposition: Lemma min_1_over_n_plus_1_to_0 : Un_cv (fun (n : ℕ) ↦ - (1 / (INR(n) + 1))) 0.
proof: Proof. By lim_d_0 it holds that (Un_cv d 0). By (CV_opp) it holds that (Un_cv (opp_seq d) (-0)) (i). It holds that ( Un_cv (fun n ↦ -d(n), -0)). It holds that ( Un_cv (fun n ↦ -(1 / (n + 1)), -0)). It holds that (0 = -0). It suffices to show that (Un_cv (fun n ↦ -(1 / (n + 1)), -0)). By (i) we conclude that (Un_cv (fun n ↦ -(1 / (n + 1)), -0)). Qed.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Tactics Automation Libs.Reals Notations