apply sq_nonneg
case neg
s : Sieve
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h_sq :
  (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0) =
    (∑ d ∈ n.divisors, weights d) ^ 2
hn : ¬n = 1
⊢ 0 ≤ (∑ d ∈ n.divisors, weights d) ^ 2
no goals