lean_workbook_plus_70306
ProvedWe have if and only if
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70306 : ∀ a : ℝ, (2 * (1 - a + a ^ 2) ^ 2 ≥ 1 + a ^ 4 ↔ (1 - a) ^ 4 ≥ 0) := by sorry
Source
We have if and only if
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_70306 : ∀ a : ℝ, (2 * (1 - a + a ^ 2) ^ 2 ≥ 1 + a ^ 4 ↔ (1 - a) ^ 4 ≥ 0) := by sorry