lean_workbook_plus_64393
ProvedIf are real numbers such that , then prove that \n \nThis is Problem 33 on pg. 532 of Pre-College Math. \n\nRather if there is any elegant way and some clever trick that may be applied is preferable, for even I have a solution by just substituting for as and then expanding everything on the LHS and RHS.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_64393 (a b c : ℝ) (h : a + b + c = 0) : (a^5 + b^5 + c^5) / 5 = (a^3 + b^3 + c^3) / 3 * (a^2 + b^2 + c^2) / 2 := by sorry
Source