have ngeN₁ : n ≥ N₁ := le_of_max_le_right ngt
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
n : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
⊢ |s n * t n - 0| < ε
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
n : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
ngeN₁ : n ≥ N₁
⊢ |s n * t n - 0| < ε