simp only [range_zero, sum_empty, abs_zero, zero_le_one]
case zero

⊢ |∑ n ∈ range 0, ↑(μ n) / ↑n| ≤ 1

case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1
case succ
N : ℕ
⊢ |∑ n ∈ range (N + 1), ↑(μ n) / ↑n| ≤ 1