lean_workbook_plus_54986

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_54986 (a b c d e : ℝ) (ha : a = 1 / 5) (hb : b = 1 / 5) (hc : c = 1 / 5) (hd : d = 1 / 5) (he : e = 1 / 5) : a * b * c * d * e + 4 ≥ a * b * c * d + a * b * c * e + a * b * d * e + a * c * d * e + b * c * d * e   :=  by sorry