lean_workbook_plus_82717
ProvedWhen we have\n\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_82717 : ∀ x : ℝ, 1 + x ^ 2 ≥ 2 * x ↔ (1 - x) ^ 2 ≥ 0 := by sorry
Source
When we have\n\n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_82717 : ∀ x : ℝ, 1 + x ^ 2 ≥ 2 * x ↔ (1 - x) ^ 2 ≥ 0 := by sorry