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