swap
case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1

case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1
case neg
s : SelbergSieve
d : ℕ
hdP : ¬d ∣ P
⊢ |s.selbergWeights d| ≤ 1

case pos
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ |s.selbergWeights d| ≤ 1