trans (∑ d in divisors P, μPlus d * s.multSum d)
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d

s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|