lean_workbook_plus_71133
ProvedIf , prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71133 (a b : ℝ) (hab : a ≥ 1 ∧ b ≥ 1) : a^5 + b^5 ≥ (a + b) * a^2 * b^2 := by sorry
Source
If , prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_71133 (a b : ℝ) (hab : a ≥ 1 ∧ b ≥ 1) : a^5 + b^5 ≥ (a + b) * a^2 * b^2 := by sorry