lean_workbook_plus_69789
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69789 (b c : ℝ) : (b + c) ^ 2 * (b - c) ^ 2 * (4 * b ^ 2 - b * c + 4 * c ^ 2) ≥ 0 := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_69789 (b c : ℝ) : (b + c) ^ 2 * (b - c) ^ 2 * (4 * b ^ 2 - b * c + 4 * c ^ 2) ≥ 0 := by sorry