apply if_neg
case neg.h
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ (if l = k * m then f l else 0) = 0
case neg.h.hnc
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : k ∣ n
m : ℕ
a✝ : m ∈ n.divisors
hdvd : ¬k * m ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ ¬l = k * m