rintro rfl
s : SelbergSieve
k m d : ℕ
hkd : k ∣ d
hk : k ∈ P.divisors
hm : m ∈ P.divisors
h : (↑k * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ k ≠ 0
s : SelbergSieve
m d : ℕ
hm : m ∈ P.divisors
hkd : 0 ∣ d
hk : 0 ∈ P.divisors
h : (↑0 * ↑m) ^ 2 ≤ y ∧ m.Coprime d
⊢ False