intros lim_infinie x lim_x
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
⊢ tendsto_infinity u → ∀ (x : ℝ), ¬seq_limit u x
u✝ : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
u : ℕ → ℝ
lim_infinie : tendsto_infinity u
x : ℝ
lim_x : seq_limit u x
⊢ False