gcongr with d hd
s : SelbergSieve
⊢ ∑ d ∈ P.divisors, |s.selbergMuPlus d| * |s.rem d| ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
case h
s : SelbergSieve
d : ℕ
hd : d ∈ P.divisors
⊢ |s.selbergMuPlus d| * |s.rem d| ≤ if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0