exact hpp.ne_zero
case hnu_lt.hnc
s : SelbergSieve
hnu : s.nu = (↑ζ).pdiv ↑ArithmeticFunction.id
hP : ∀ (p : ℕ), p.Prime → ↑p ≤ s.level → p ∣ s.prodPrimes
p : ℕ
hpp : p.Prime
a✝ : p ∣ s.prodPrimes
⊢ ¬p = 0
no goals