lean_workbook_plus_6452
Disprovedequivalent to
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6452 : ∀ x y : ℝ, (x - y) ^ 2 * (x ^ 2 * y ^ 3 + 2 * x + y) / y ^ 3 ≥ 0 := by sorry
Source
equivalent to
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_6452 : ∀ x y : ℝ, (x - y) ^ 2 * (x ^ 2 * y ^ 3 + 2 * x + y) / y ^ 3 ≥ 0 := by sorry