lean_workbook_plus_12952
ProvedProve that if then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12952 (a : ℝ) (h : a > 1) : (a - 1)⁻¹ + a⁻¹ + (a + 1)⁻¹ > 3 * a⁻¹ := by sorry
Source
Prove that if then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_12952 (a : ℝ) (h : a > 1) : (a - 1)⁻¹ + a⁻¹ + (a + 1)⁻¹ > 3 * a⁻¹ := by sorry