lean_workbook_plus_5807
DisprovedProve that : + ≥ where >0
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5807 : ∀ a b : ℝ, a > 0 ∧ b > 0 → a^2 + b^2 + b^2 / a^2 ≥ a / b + b / a := by sorry
Source
Prove that : + ≥ where >0
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_5807 : ∀ a b : ℝ, a > 0 ∧ b > 0 → a^2 + b^2 + b^2 / a^2 ≥ a / b + b / a := by sorry