Preferred representation of a polynomial

[Stanislas Polu]

Hi!

I've been playing with a proof[0] about the sum of roots of a simple
polynomial and wanted to use `vieta1`. I landed on the following
representation:

( ph -> sum_ y e. ( `' ( z e. CC |-> sum_ k e. ( 0 ... 2 ) ( ( <" -u 6
3 9 "> ` k ) x. ( z ^ k ) ) ) " { 0 } ) y = -u ( 3 / 9 ) )

and demonstrated its equality to the original polynomial:

```
( z e. CC |-> ( ( ( 9 x. ( z ^ 2 ) ) + ( 3 x. z ) ) - 6 ) )
```

But deep in the weeds of the proof I realize that the use of a `Word`
is quite unfortunate, as `vieta1` (through `coeff`) and `dgrval`
expect the coefficients to be defined over NN0 and not a finite
sequence.

I was curious to hear from folks what is the preferred/recommended way
to represent a particular polynomial to use with these theorems?

Thanks thanks and hope you have a wonderful break!

-stan

[0] AMC 12 2000 p15
```
|- ( ph -> F : CC --> CC )
|- ( ph -> A. x e. CC ( F ` ( x / 3 ) ) = ( ( ( x ^ 2 ) + x ) + 1 ) )
|- ( ph -> sum_ y e. ( `' F " { 7 } ) ( y / 3 ) = -u ( 1 / 9 ) )
```