apply fun hkl => hkn <| hkl.trans (dvd_of_mem_divisors hl)
case neg
s : SelbergSieve
k n : ℕ
f : ℕ → ℝ
h : ∀ (l : ℕ), l ∣ n → ¬k ∣ l → f l = 0
hn : ¬n = 0
hkn : ¬k ∣ n
l : ℕ
hl : l ∈ n.divisors
⊢ ¬k ∣ l
no goals