fact: Definition is_seq_acc_pt (a : ℕ → ℝ) (x : ℝ) : Prop := ∃ n : ℕ → ℕ, is_index_seq n ∧ Un_cv (fun (k : ℕ) ↦ a(n k)) x.
imports: Coq.Reals.Reals Lra Classical Classical_Pred_Type ClassicalChoice Automation Libs.Analysis.Sequences Libs.Analysis.Subsequences Notations Tactics