poly_rew : THEORY
BEGIN

  IMPORTING polynomials

  p,q : VAR sequence[real]
  x,k : VAR real
  n   : VAR nat

  poly_sum : LEMMA
    polynomial(p,n)(x)+polynomial(q,n)(x) = polynomial(p+q,n)(x)

  poly_neg : LEMMA
   -polynomial(p,n)(x) = polynomial(-p,n)(x) 

  poly_diff : LEMMA
    polynomial(p,n)(x)-polynomial(q,n)(x) = polynomial(p-q,n)(x)

  poly_scal : LEMMA 
    k*polynomial(p,n)(x) = polynomial(k*p,n)(x)

END poly_rew