apply _root_.add_le_add (le_rfl)
s : Sieve
μPlus : UpperBoundSieve
⊢ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤ ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|