lean_workbook_plus_7915
ProvedFinally, the inequality can be rewritten as:\n\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7915 (u v : ℝ) : (u^3 - u^2 * v - 2 * u * v^2 + v^3)^2 ≥ 0 := by sorry
Source
Finally, the inequality can be rewritten as:\n\n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_7915 (u v : ℝ) : (u^3 - u^2 * v - 2 * u * v^2 + v^3)^2 ≥ 0 := by sorry