specialize h n
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 N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
⊢ |v n - l| ≤ ε
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
h' : ∀ (n : ℕ), v n ≤ w n
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : |u n - l| ≤ ε
hN' : |w n - l| ≤ ε
h : u n ≤ v n
⊢ |v n - l| ≤ ε