import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}

def SeqLim (u : ℕ → ℝ) (a : ℝ) : Prop :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def SeqConv (u : ℕ → ℝ) :=
  ∃ a, SeqLim u a

def IsCauchy (u : ℕ → ℝ) :=
  ∀ ε > 0, ∃ k, ∀ p ≥ k, ∀ q ≥ k, |u p - u q| < ε

example
  (h : SeqConv u)
  : IsCauchy u :=
by sorry