have hp_prime : p.Prime := prime_of_mem_primeFactors hp
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 - ν p
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
⊢ 0 < 1 - ν p