use max N N'
case intro.intro
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∃ N, ∀ n ≥ N, |v n - l| ≤ ε
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h : ∀ (n : ℕ), u n ≤ v n
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
N' : ℕ
hN' : ∀ n ≥ N', |w n - l| ≤ ε
⊢ ∀ n ≥ max N N', |v n - l| ≤ ε