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!

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.
