have hp_dvd : p ∣ P := (Nat.dvd_of_mem_primeFactors hp).trans hl
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
⊢ 0 < 1 - ν p
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
hp_dvd : p ∣ P
⊢ 0 < 1 - ν p