lean_workbook_plus_29255

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_29255 (x1 x2 x3 : ℝ) (hx1 : 0 < x1) (hx2 : 0 < x2) (hx3 : 0 < x3) (hx : x1 + x2 + x3 = 1) : x1 * x2 + x1 * x3 + x2 * x3 ≤ 1 / 3   :=  by sorry