constructor <;> linarith
case h
u v w : ℕ → ℝ
l : ℝ
hu : seq_limit u l
hw : seq_limit w l
ε : ℝ
ε_pos : ε > 0
N N' n : ℕ
hn : n ≥ N ∧ n ≥ N'
hN : -ε ≤ u n - l ∧ u n - l ≤ ε
hN' : -ε ≤ w n - l ∧ w n - l ≤ ε
h : u n ≤ v n
h' : v n ≤ w n
⊢ -ε ≤ v n - l ∧ v n - l ≤ ε
no goals