An inequality for real exponential sums

Let $a,b,c \in R$ and $a+b+c=0$ . Prove that $\boxed{8^a+8^b+8^c\ge 2^a+2^b+2^c}$

Declaration repair: Added explicit real binders (a b c : ℝ) and real base annotations so every variable exponent uses Real.rpow. The old simp proof depended on natural-number inference and does not prove this repaired theorem. A new argument proves the intended real-exponent inequality.

Source: InternLM Lean-Workbook, record lean_workbook_plus_44637 (Apache-2.0). Original malformed declaration. This record proves the corrected statement.