# REAL_POLY_CONV
`((x1 + x2) pow 4 + (x1 + x3) pow 4 + (x1 + x4) pow 4 +
(x2 + x3) pow 4 + (x2 + x4) pow 4 + (x3 + x4) pow 4) / &6 +
((x1 - x2) pow 4 + (x1 - x3) pow 4 + (x1 - x4) pow 4 +
(x2 - x3) pow 4 + (x2 - x4) pow 4 + (x3 - x4) pow 4) / &6 -
(x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2`;;
val it : thm =
|- ((x1 + x2) pow 4 +
(x1 + x3) pow 4 +
(x1 + x4) pow 4 +
(x2 + x3) pow 4 +
(x2 + x4) pow 4 +
(x3 + x4) pow 4) /
&6 +
((x1 - x2) pow 4 +
(x1 - x3) pow 4 +
(x1 - x4) pow 4 +
(x2 - x3) pow 4 +
(x2 - x4) pow 4 +
(x3 - x4) pow 4) /
&6 -
(x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2 =
&0