lean_workbook_plus_6407
Provednow if then it is obviously true, so let then we have to show or
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6407 (b a : ℝ) (ha : a ≠ 0) : |1 + b / a| + 2 * |1 - b / a| ≥ 2 := by sorry
Source