Asymmetric Inequality
Let $a, b, c$ be positive real numbers such that $\frac{1}{a} + \frac{1}{b} + \frac{1}{c} = 1$. Show that $$a + b + c \le \sqrt{b ^ 3 + a c ^ 2 + a ^ 2 c}.$$
Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.
import Mathlib.Data.Real.Sqrt
theorem solution (a b c : ℝ) (ha : a > 0) (hb : b > 0) (hc : c > 0)
(h : 1 / a + 1 / b + 1 / c = 1) : a + b + c ≤ √ (b ^ 3 + a * c ^ 2 + a ^ 2 * c) := sorry
Login to submit a solution.