Lean-Workbook Plus 37788: Trigonometric inequality
ProvedWorkbookRestored.plus_37788lean-workbookrestored-importssource-checked
For , .
Source: Lean-Workbook row lean_workbook_plus_37788 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.
Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic open Real
Formal statement
theorem WorkbookRestored.plus_37788 {A B C : ℝ} (hA : 0 < A ∧ A ≤ π ∧ B ≤ π ∧ C ≤ π) (hB : 0 < B ∧ B ≤ π ∧ A ≤ π ∧ C ≤ π) (hC : 0 < C ∧ C ≤ π ∧ A ≤ π ∧ B ≤ π) : 9 / 4 + Real.cos A ^ 2 + Real.cos B ^ 2 + Real.cos C ^ 2 ≥ Real.cos A + Real.cos B + Real.cos C := by sorrySource