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

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

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