apply sum_congr rfl
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d =
    ∑ x ∈ P.divisors, (X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x)
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ x ∈ P.divisors, μPlus.μPlus x * s.multSum x = X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x