lean_workbook_plus_68452
Provedprove that:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68452 (a b c : ℝ) : (b^2+c^2-a^2)*(b-c)^2+(-b^2+a^2+c^2)*(c-a)^2+(b^2+a^2-c^2)*(a-b)^2 ≥ 0 := by sorry
Source
prove that:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_68452 (a b c : ℝ) : (b^2+c^2-a^2)*(b-c)^2+(-b^2+a^2+c^2)*(c-a)^2+(b^2+a^2-c^2)*(a-b)^2 ≥ 0 := by sorry