exact le_of_lt (hN n hn)
case h
u✝ : ℕ → ℝ
l : ℝ
φ✝ : ℕ → ℕ
a b : ℝ
u : ℕ → ℝ
h : ∀ (n : ℕ), u n ∈ Icc a b
c : ℝ
c_in : c ∈ Icc a b
φ : ℕ → ℕ
hφ : StrictMono φ
lim : ∀ ε > 0, ∃ a, ∀ b ≥ a, |((fun n => u n) ∘ φ) b - c| < ε
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ b ≥ N, |((fun n => u n) ∘ φ) b - c| < ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - c| ≤ ε
no goals