lean_workbook_plus_61766
Provedthen just need check \n\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61766 : ∀ x : ℝ, (1 - x ^ 2) + (1 - x) ^ 2 / 4 ≤ 4 / 3 := by sorry
Source
then just need check \n\n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_61766 : ∀ x : ℝ, (1 - x ^ 2) + (1 - x) ^ 2 / 4 ≤ 4 / 3 := by sorry