lean_workbook_plus_50585
ProvedSquaring and C-S: .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_50585 (a b c : ℝ) : Real.sqrt ((a^2 + b^2) * (a^2 + c^2)) ≥ a^2 + b * c := by sorry
Source
Squaring and C-S: .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_50585 (a b c : ℝ) : Real.sqrt ((a^2 + b^2) * (a^2 + c^2)) ≥ a^2 + b * c := by sorry