trans ((μ d :ℝ)^2 * (ν d)⁻¹ * g d * S⁻¹ * ∑ m in divisors P,
        if (d * m) ^ 2 ≤ y ∧ Coprime m d then g m else 0)
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ((∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) * ↑(μ d))
s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ 0 ≤ ↑(μ d) ^ 2 * (ν d)⁻¹ * g d * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0

s : SelbergSieve
d : ℕ
hdP : d ∣ P
⊢ (↑(μ d) ^ 2 * (ν d)⁻¹ * g d * S⁻¹ * ∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) ≤
    (ν d)⁻¹ * g d * ↑(μ d) * S⁻¹ * ((∑ m ∈ P.divisors, if (↑d * ↑m) ^ 2 ≤ y ∧ m.Coprime d then g m else 0) * ↑(μ d))