lean_workbook_plus_13644
DisprovedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13644 : ∀ p q x : ℝ, p^2*q - 2*p*q*x + q*x^2 ≥ -p^2*q + 2*p*q*x - q*x^2 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_13644 : ∀ p q x : ℝ, p^2*q - 2*p*q*x + q*x^2 ≥ -p^2*q + 2*p*q*x - q*x^2 := by sorry