lean_workbook_plus_17596
ProvedLet , and be non-negative numbers. Prove that:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17596 (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) : 2 * (a ^ 3 + b ^ 3 + c ^ 3) + 3 ≥ 3 * (a * b + a * c + b * c) := by sorry
Source