intros ε ε_pos
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
⊢ ∀ ε > 0, |l - l'| ≤ ε
case a
u : ℕ → ℝ
l l' : ℝ
hl : seq_limit u l
hl' : seq_limit u l'
ε : ℝ
ε_pos : ε > 0
⊢ |l - l'| ≤ ε