`INT_POLY_CONV : term -> thm`

SYNOPSIS
Converts a integer polynomial into canonical form.

DESCRIPTION
Given a term of type :int that is built up using addition, subtraction, negation and multiplication, INT_POLY_CONV converts it into a canonical polynomial form and returns a theorem asserting the equivalence of the original and canonical terms. The basic elements need not simply be variables or constants; anything not built up using the operators given above will be considered `atomic' for the purposes of this conversion. The canonical polynomial form is a `multiplied out' sum of products, with the monomials (product terms) ordered according to the canonical OCaml order on terms. In particular, it is just &0 if the polynomial is identically zero.

FAILURE CONDITIONS
Never fails, even if the term has the wrong type; in this case it merely returns a reflexive theorem.

EXAMPLE
This illustrates how terms are `multiplied out':
```  # INT_POLY_CONV `(x + y) pow 3`;;
val it : thm =
|- (x + y) pow 3 = x pow 3 + &3 * x pow 2 * y + &3 * x * y pow 2 + y pow 3
```
while the following verifies a remarkable `sum of cubes' identity due to Yasutoshi Kohmoto:
```  # INT_POLY_CONV
`(&1679616 * a pow 16 - &66096 * a pow 10 * b pow 6 +
&153 * a pow 4 * b pow 12) pow 3 +
(-- &1679616 * a pow 16 - &559872 * a pow 13 * b pow 3 -
&27216 * a pow 10 * b pow 6 + &3888 * a pow 7 * b pow 9 +
&63 * a pow 4 * b pow 12 - &3 * a * b pow 15) pow 3 +
(&1679616 * a pow 15 * b + &279936 * a pow 12 * b pow 4 -
&11664 * a pow 9 * b pow 7 -
&648 * a pow 6 * b pow 10 + &9 * a pow 3 * b pow 13 + b pow 16) pow 3`;;
val it : thm =
|- ... =
b pow 48
```

USES
Keeping terms in normal form. For simply proving equalities, INT_RING is more powerful and usually more convenient.