apply le_of_pow_le_pow_left two_ne_zero (by positivity)
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 4 + b ^ 4 + c ^ 4
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)) ^ 2 ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2