let a, b be positive Real; :: thesis: (a |^ 4) + (b |^ 4) >= ((a |^ 3) * b) + (a * (b |^ 3))
(a - b) ^2 >= 0 by XREAL_1:63;
then ((a - b) * (a - b)) * (((a ^2) + (a * b)) + (b ^2)) >= 0 ;
then (a - b) * ((a - b) * (((a ^2) + (a * b)) + (b ^2))) >= 0 ;
then (a - b) * ((a |^ 3) - (b |^ 3)) >= 0 by Lm1;
then (((a |^ 3) * a) - ((a |^ 3) * b)) - ((b |^ 3) * (a - b)) >= 0 ;
then ((a |^ (3 + 1)) - ((a |^ 3) * b)) - ((b |^ 3) * (a - b)) >= 0 by NEWTON:6;
then ((a |^ 4) - ((a |^ 3) * b)) - (((b |^ 3) * a) - ((b |^ 3) * b)) >= 0 ;
then ((a |^ 4) - ((a |^ 3) * b)) - (((b |^ 3) * a) - (b |^ (3 + 1))) >= 0 by NEWTON:6;
then ((((a |^ 4) + (b |^ 4)) - ((a |^ 3) * b)) - ((b |^ 3) * a)) + (((a |^ 3) * b) + ((b |^ 3) * a)) >= 0 + (((a |^ 3) * b) + ((b |^ 3) * a)) by XREAL_1:7;
hence (a |^ 4) + (b |^ 4) >= ((a |^ 3) * b) + (a * (b |^ 3)) ; :: thesis: verum