lean_workbook_plus_12542
OpenThe inequality simplifies further to .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12542 (r₁ r₂ : ℝ) (θ : ℝ) : (1 - Real.cos θ) * (r₁ - r₂) ^ 2 ≥ 0 := by sorry
Source
The inequality simplifies further to .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_12542 (r₁ r₂ : ℝ) (θ : ℝ) : (1 - Real.cos θ) * (r₁ - r₂) ^ 2 ≥ 0 := by sorry