lean_workbook_plus_920

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_920 : ∀ a b c d k : ℝ, k < 3 → 2 * (a * b + b * c + c * d + d * a + a * c + b * d) ≤ a + b + c + d + k * (a * b * c + a * b * d + a * c * d + b * c * d)   :=  by sorry