cases' lim_infinie (x+2) with N' hN'
case intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
⊢ False
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N : ℕ
hN : ∀ n ≥ N, |u n - x| ≤ 1
N' : ℕ
hN' : ∀ n ≥ N', u n ≥ x + 2
⊢ False