have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
⊢ 0 < ν p
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : p.Prime
⊢ 0 < ν p