lean_workbook_plus_66143
ProvedLet be reals such that Prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66143 (x y : ℝ) (h : x^2 - 4*x*y - y^2 = 5) : 2*x^2 + 3*y^2 ≥ 5 := by sorry
Source
Let be reals such that Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_66143 (x y : ℝ) (h : x^2 - 4*x*y - y^2 = 5) : 2*x^2 + 3*y^2 ≥ 5 := by sorry