For $a^3+b^3+c^3=3$ prove that $a^4b+b^4c+c^4a\leq3$ 
Let $a$, $b$ and $c$ be non-negative numbers such that $a^3+b^3+c^3=3$. Prove that:
  $$a^4b+b^4c+c^4a\leq3$$

This inequality similar to the following.

Let $a$, $b$ and $c$ be non-negative numbers such that $a^2+b^2+c^2=3$. Prove that:
  $$a^3b+b^3c+c^3a\leq3,$$
  which follows from the following identity.
  $$(a^2+b^2+c^2)^2-3(a^3b+b^3c+c^3a)=\frac{1}{2}\sum_{cyc}(a^2-b^2-ab-ac+2bc)^2.$$

I tried Rearrangement.
Let $\{a,b,c\}=\{x,y,z\}$, where $x\geq y\geq z$.
Hence, $$a^4b+b^4c+c^4a=a^3\cdot ab+b^3\cdot bc+c^3\cdot ca\leq x^3\cdot xy+y^3\cdot xz+z^3\cdot yz=$$
$$=y(x^4+y^2xz+z^4)$$
and I don't see what is the rest.
Thank you!
 A: Since $(a,b,c)$ is restricted to a compact set, it follows that $F_2 := a^4b +b^4 c + c^4 a$ has a maximal value, which must either be at an endpoint (i.e. one of $a,b,c$ is $0$, but these cases are easily eliminated) or at a point where the derivatives vanish.
Let $F_1 := a^3+b^3+c^3$. If we keep $c$ fixed and equate $F_1$ to $3$, then $b$ is a function of $a$, and we can use this to differentiate $F_2$ with respect to $a$. Equating that derivative to $0$ gives an equation. We can do the same with the roles of $a,b,c$ rotated and we get three equations:
$E = \{-a^6+4a^3b^3-4a^2b^3c+b^2c^4 = 0, 4a^3bc^2-4a^3c^3-a^2b^4+c^6 = 0, a^4c^2-4ab^2c^3-b^6+4b^3c^3 = 0\}$
To maximize $F_2$ under $F_1 = 3$, solve the equations $E \bigcup \{F_1 = 3\}$ (I need a computer for this step). These equations have 84 solutions. Most of them are complex. The only real solutions are $\{a,b,c\} = \{-0.26829, 0.80474, 1.3569\}$ and $\{a,b,c\}=1$. The only non-negative solution of $E \bigcup \{F_1 = 3\}$ is $a=b=c=1$.  So that is where $F_2$ takes its maximum.
I have to ask: where did the problem come from, and was it formulated in a way that indicates that there should also be an answer that can be found with human-only computation?  One way to reduce the computation would be to solve $E \bigcup \{F_1=3, F_2=3\}$ (only solution is $a=b=c=1$) (unlike my first method, it would be possible to produce a human-verifyable proof for this) and then consider derivatives at this point to show that this is a local maximum of $F_2$. That would produce a proof with computations short enough to be human-verifyable, though it still wouldn't be a nice proof.
A: The Buffalo Way works. However it is not nice.
Let me describe Michael Rozenberg's solution. We have
\begin{align}
\sum_{\mathrm{cyc}} a^4b &\le \frac{1}{3}\sum_{\mathrm{cyc}} (a^{9/2}b^{3/2} + a^{9/2}b^{3/2} + a^3)\\
&= \frac{2}{3} \sum_{\mathrm{cyc}} a^{9/2}b^{3/2} + \frac{1}{3} (a^3+b^3+c^3)\\
&\le \frac{2}{9} (a^3+b^3+c^3)^2 + \frac{1}{3} (a^3+b^3+c^3)\\
&= 3
\end{align}
where we have used Vasc's inequality $(x^2+y^2+z^2)^2\ge 3(x^3y+y^3z+z^3x)$
to obtain $\sum_{\mathrm{cyc}} a^{9/2}b^{3/2} \le \frac{1}{3}(a^3+b^3+c^3)^2$.
This inequality can be used to prove the following inequality:
Let $x,y,z>0$ and $x^7+y^7+z^7=3$. Prove that
$\frac{x^4}{y^3}+\frac{y^4}{z^3}+\frac{z^4}{x^3}\ge 3$.
Proof: Using AM-GM, we have $7\frac{x^4}{y^3} + 9 x^{28/3} y^{7/3} \ge 16 x^7$
which results in $$7 \sum_{\mathrm{cyc}} \frac{x^4}{y^3} + 9 \sum_{\mathrm{cyc}} x^{28/3} y^{7/3} \ge 16 (x^7+y^7+z^7). $$
It suffices to prove that $\sum_{\mathrm{cyc}} x^{28/3} y^{7/3} \le 3$.
Let $a = x^{7/3}, \ b = y^{7/3}, \ c = z^{7/3}$. The condition becomes $a^3+b^3+c^3 = 3$.
We need to prove that $a^4b+b^4c+c^4a \le 3$. We are done.
