lean_workbook_plus_69836

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_69836 (n : ℕ) (a : ℝ) (x : ℕ → ℝ) (h₁ : ∀ i ∈ Finset.range n, 0 ≤ x i) (h₂ : ∀ i ∈ Finset.range n, x i ≤ a) : ∑ i in Finset.range n, x i * (x i - a) ≤ 0   :=  by sorry