# INT_RING
`!a b c:int.
a + b + c = &0
==> &2 * (a * b + a * c + b * c) pow 2 =
a pow 4 + b pow 4 + c pow 4 /\
&2 * (a * b + a * c + b * c) pow 4 =
(a * (b - c)) pow 4 + (b * (a - c)) pow 4 + (c * (a - b)) pow 4`;;
...
val it : thm =
|- !a b c.
a + b + c = &0
==> &2 * (a * b + a * c + b * c) pow 2 = a pow 4 + b pow 4 + c pow 4 /\
&2 * (a * b + a * c + b * c) pow 4 =
(a * (b - c)) pow 4 + (b * (a - c)) pow 4 + (c * (a - b)) pow 4
The reasoning # INT_RING
`(x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) *
(y1 pow 2 + y2 pow 2 + y3 pow 2 + y4 pow 2) =
(x1 * y1 - x2 * y2 - x3 * y3 - x4 * y4) pow 2 +
(x1 * y2 + x2 * y1 + x3 * y4 - x4 * y3) pow 2 +
(x1 * y3 - x2 * y4 + x3 * y1 + x4 * y2) pow 2 +
(x1 * y4 + x2 * y3 - x3 * y2 + x4 * y1) pow 2`;;
...
Note that formulas depending on specific features of the integers are not
always provable by this generic ring procedure. For example we cannot prove: