rw[hnu]
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ s.nu n
case hnu_nonneg
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
n : ℕ
⊢ 0 ≤ ((↑ζ).pdiv ↑ArithmeticFunction.id) n