lean_workbook_plus_8773
ProvedProve that for non-negative and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8773 (u v : ℝ) (hu : u ≥ 0) (hv : v ≥ 0) : u^3 - u * v^2 + v^3 ≥ 0 := by sorry
Source
Prove that for non-negative and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_8773 (u v : ℝ) (hu : u ≥ 0) (hv : v ≥ 0) : u^3 - u * v^2 + v^3 ≥ 0 := by sorry