fact: Definition is_accumulation_point (p : X) (a : ℕ → X) := ∃ m : (ℕ → ℕ), is_index_sequence m ∧ (a ◦ m) ⟶ p.
imports: Coq.Reals.Reals Automation Libs.Analysis.MetricSpaces Libs.Analysis.SequencesMetric Notations Tactics