lean_workbook_plus_46460
ProvedProve that for ,\n
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_46460 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → a^2 + (-2*c + 3*b)*a + b^2 + c^2 - b*c ≥ 0 := by sorry
Source
Prove that for ,\n
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_46460 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → a^2 + (-2*c + 3*b)*a + b^2 + c^2 - b*c ≥ 0 := by sorry