lean_workbook_plus_37870

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_37870 :  ∀ a b c : ℝ, a * b * c ≤ 1 → a^2 * b^2 * c^2 + a * b * c + a * b * c * (a * b + b * c + c * a) + a * b * c * (a + b + c) ≤ a^2 + b^2 + c^2 + a + b + c + 2   :=  by sorry