linarith
case intro.intro
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
N N' : ℕ
N₀ : ℕ := max N N'
hN : -1 ≤ u N₀ - x ∧ u N₀ - x ≤ 1
hN' : u N₀ ≥ x + 2
⊢ False
no goals