fact: Definition series_cv_abs_to (a : ℕ → ℝ) (l : ℝ) := series_cv_to (fun n ↦ Rabs(a n)) l.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Analysis.Sequences Notations Tactics