revert hnu_nonzero
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν d ≠ 0
case a
s : Sieve
l : ℕ
hl : Squarefree l
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ν l ≠ 0 → ν d ≠ 0