fact: Definition convergence {M : Metric_Space} (a : ℕ → Base M) (c : Base M) := ∀ ε : ℝ, ε > 0 ⇒ ∃ N1 : ℕ, ∀ n : ℕ, (n ≥ N1)%nat ⇒ dist M (a n) c < ε.
imports: Coq.Reals.Reals Automation Libs.Negation Notations Tactics