rw [div_le_div_iff (by positivity) (by positivity)]
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 / (a ^ 4 + b ^ 4 + c ^ 4) ≤ a ^ 3 / √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4)