lean_workbook_plus_67827
ProvedIf prove that: .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67827 (a : ℝ) (h : a > 0) : a - 1 / 4 ≤ (a^2 + 2) ^ 2 / (2 * Real.sqrt 3) ^ 2 := by sorry
Source
If prove that: .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_67827 (a : ℝ) (h : a > 0) : a - 1 / 4 ≤ (a^2 + 2) ^ 2 / (2 * Real.sqrt 3) ^ 2 := by sorry