Quelle  more_polynomial_props.pvs

more_polynomial_props: THEORY
BEGIN

  IMPORTING polynomials,sign,log_nat,min_max

  a,b,h : VAR sequence[real]
  n   : VAR nat
  m,p   : VAR nat
  x,y,z : VAR real

  polynomial_degree_existence: LEMMA
    ((EXISTS (x): polynomial(a,n)(x)/=0) OR
     (EXISTS (i:upto(n)): a(i)/=0))
    IMPLIES
    EXISTS (i:upto(n)): a(i)/=0 AND
      (FORALL (j:nat): j>i AND j<=n IMPLIES a(j) = 0) AND
      polynomial(a,n) = polynomial(a,i)

  square_free?(a,n): bool =
    FORALL (y:real,g:sequence[real],k:nat): polynomial(a,n)(y)=0 AND
      (FORALL (x:real): polynomial(a,n)(x) = (x-y)*polynomial(g,k)(x))
      IMPLIES
      polynomial(g,k)(y)/=0

  poly_deriv_limit: LEMMA
    FORALL (y:real,epsil:posreal,pn:posnat): EXISTS (delta:posreal):
      FORALL (x:real): abs(x-y)<delta AND x/=y IMPLIES
        abs(polynomial(poly_deriv(a),pn-1)(y) - 
     (polynomial(a,pn)(x)-polynomial(a,pn)(y))/(x-y)) < epsil

  square_free_min: LEMMA
    FORALL (epsil:posreal,y,c:real,pn:posnat): polynomial(a,pn)(y) = c AND 
   (FORALL (x:real): abs(x-y)<epsil IMPLIES polynomial(a,pn)(x)>=c)
   IMPLIES
   polynomial(poly_deriv(a),pn-1)(y) = 0
    
  square_free_max: LEMMA
    FORALL (epsil:posreal,y,c:real,pn:posnat): polynomial(a,pn)(y) = c AND 
   (FORALL (x:real): abs(x-y)<epsil IMPLIES polynomial(a,pn)(x)<=c)
   IMPLIES
   polynomial(poly_deriv(a),pn-1)(y) = 0


  IMPORTING binomial_identities

  deriv_poly_shift: LEMMA n>0 AND (FORALL (i:nat):i>n IMPLIES a(i)=0)
           IMPLIES
     poly_deriv(poly_shift(a,n)(y)) =
           poly_shift(poly_deriv(a),n-1)(y)

  linear_power_is_differentiable: LEMMA
    m>0 IMPLIES EXISTS (a): a(m)=1 AND
    (FORALL (i:nat): i>m IMPLIES a(i)=0) AND
    (FORALL (x): polynomial(a,m)(x) = (x-y)^m) AND
    (FORALL (x): polynomial(poly_deriv(a),m-1)(x)=m*(x-y)^(m-1))

  polynomial_prod_degrees: LEMMA
    FORALL (a,b,g:[nat->real],n,m,p:nat):
    (FORALL (x): polynomial(a,n)(x) = polynomial(b,m)(x)*polynomial(g,p)(x)) AND
    a(n)/=0 AND b(m)/=0 AND g(p)/=0 IMPLIES
    (n=m+p AND FORALL (i:nat): i<=n IMPLIES a(i) = polynomial_prod(b,m,g,p)(i))

  polynomial_div_linear_power_degree: LEMMA
    FORALL (a,b:[nat->real],n,m,k:nat):
      (FORALL (x): polynomial(a,n)(x) = (x-y)^k*polynomial(b,m)(x)) AND
      a(n)/=0 AND b(m)/=0
      IMPLIES
      (a(n)=b(m) AND n=m+k)

  poly_deriv_signs_neq_around_root_left: LEMMA n>0 AND
    x < y AND 
    polynomial(a,n)(y) = 0 AND
    (FORALL (z:real): x<=z AND z<=y AND 
                (polynomial(a,n)(z)=0 OR polynomial(poly_deriv(a),n-1)(z)=0)
        IMPLIES z=y)
    IMPLIES sign_ext(polynomial(a,n)(x)) = -sign_ext(polynomial(poly_deriv(a),n-1)(x))

  poly_deriv_signs_neq_around_root_right: LEMMA n>0 AND
    x > y AND 
    polynomial(a,n)(y) = 0 AND
    (FORALL (z:real): y<=z AND z<=x AND 
                (polynomial(a,n)(z)=0 OR polynomial(poly_deriv(a),n-1)(z)=0)
        IMPLIES z=y)
    IMPLIES sign_ext(polynomial(a,n)(x)) = sign_ext(polynomial(poly_deriv(a),n-1)(x))

  % Every polynomial is divisible by a maximal power (x-y)^m

  max_linear_div_power?(a,n,y)(m:posnat): bool =
    EXISTS (b,q:[nat->real]): m<=n AND
      (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,n-m)(x)) AND
      polynomial(b,n-m)(y)/=0 AND
      (FORALL (x): polynomial(poly_deriv(a),n-1)(x) = (x-y)^(m-1)*polynomial(q,n-m)(x)) AND
      polynomial(q,n-m)(y)/=0

  max_linear_div_power_rew: LEMMA FORALL (m:posnat):
    max_linear_div_power?(a,n,y)(m) IFF
    (m<=n AND EXISTS (b:[nat->real]):
      (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,n-m)(x)) AND
       polynomial(b,n-m)(y)/=0)

  max_linear_div_power_rew2: LEMMA FORALL (m:posnat):
    max_linear_div_power?(a,n,y)(m) IFF
    (EXISTS (b:[nat->real],k:nat):
      (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,k)(x)) AND
       polynomial(b,k)(y)/=0)

  max_linear_div_power_unique: LEMMA FORALL (m,kp:posnat):
    max_linear_div_power?(a,n,y)(m) AND
    max_linear_div_power?(a,n,y)(kp)
    IMPLIES
    m=kp

  max_linear_div_power_additive: LEMMA FORALL (m,kp:posnat,b:[nat->real],k:nat):
    max_linear_div_power?(b,k,y)(kp) AND
    (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,k)(x))
    IMPLIES
    max_linear_div_power?(a,n,y)(m+kp)

  max_linear_div_power_derivative: LEMMA
    FORALL (m:posnat): m>1 IMPLIES
      (max_linear_div_power?(a,n,y)(m) IMPLIES
      (n>0 AND max_linear_div_power?(poly_deriv(a),n-1,y)(m-1)))

  % compute_max_lin_div_pow(a,(n|a(n)/=0),y): RECURSIVE {k:nat| 
  %   (k=0 IMPLIES polynomial(a,n)(y)/=0) AND
  %   (k>0 IMPLIES max_linear_div_power?(a,n,y)(k))} =
  %     IF polynomial(a,n)(y)/=0 THEN 0
  %     ELSIF n = 1 THEN 1
  %     ELSIF 

  poly_max_zero_power: LEMMA polynomial(a,n)(y)=0 AND a(n)/=0 IMPLIES
    EXISTS (m:posnat): max_linear_div_power?(a,n,y)(m)

  max_linear_div_power_scal: LEMMA FORALL (nz:nzreal,m:posnat):
    max_linear_div_power?(a,n,y)(m) IFF
    max_linear_div_power?(nz*a,n,y)(m)

  max_linear_div_power_lower_bound: LEMMA FORALL (b:[nat->real],k,j:nat,m:posnat):
    max_linear_div_power?(a,n,y)(m) AND
    (FORALL (x): polynomial(a,n)(x)=(x-y)^k*polynomial(b,j)(x))
    IMPLIES
    k<=m AND (k=m IFF polynomial(b,j)(y)/=0)

  div_linear_power_reduces: LEMMA FORALL (b:[nat->real],k,j,d:nat):
    (FORALL (x): polynomial(a,n)(x) = (x-y)^k*polynomial(b,j)(x))
    AND k>=d IMPLIES
    (EXISTS (bb:[nat->real],q:nat): 
      FORALL (x): polynomial(a,n)(x) = (x-y)^d*polynomial(bb,q)(x))

  max_linear_div_power_sign_change: LEMMA FORALL (m:posnat):
    x < y AND y < z AND
    (FORALL (r:real): x<= r AND r<= z AND polynomial(a,n)(r) = 0
         IMPLIES r = y) AND
    max_linear_div_power?(a,n,y)(m)
    IMPLIES
    LET sigx = sign_ext(polynomial(a,n)(x)), sigz = sign_ext(polynomial(a,n)(z)) IN
      sigx/=0 AND sigz/=0 AND
      ((even?(m) AND (NOT odd?(m)) AND sigx = sigz AND sigx/=-sigz)
       OR
       (odd?(m) AND (NOT even?(m)) AND sigx = -sigz AND sigx/=sigz))

  poly_eq_except_on_finite_set: LEMMA FORALL (b:[nat->real]):
    FORALL (N:posnat): (EXISTS (rootseq:[below(N)->real]): 
        FORALL (x): (FORALL (ib:below(N)): x/=rootseq(ib)) IMPLIES
    polynomial(a,n)(x)=polynomial(b,m)(x))
    IMPLIES ((FORALL (j:nat): j<=n AND j>min(n,m) IMPLIES a(j)=0) AND
         (FORALL (j:nat): j<=m AND j>min(n,m) IMPLIES b(j)=0) AND
     (FORALL (j:nat): j<=min(n,m) IMPLIES a(j) = b(j)) AND
     polynomial(a,n) = polynomial(b,m))

  max_div_linear_power_remainder_sign_swaps: LEMMA
    FORALL (p,q,h,r:[nat->real],pn,qn,hn,rn:nat,m,kp:posnat):
    x<y AND y<z AND
    (FORALL (xyz:real): polynomial(p,pn)(xyz)=
      polynomial(q,qn)(xyz)*polynomial(h,hn)(xyz)
        +polynomial(r,rn)(xyz)) AND
    (FORALL (xyz:real): x<=xyz AND xyz<=z AND
      (polynomial(p,pn)(xyz)=0 OR polynomial(h,hn)(xyz)=0 OR polynomial(r,rn)(xyz)=0)
      IMPLIES xyz = y) AND
    max_linear_div_power?(p,pn,y)(m) AND
    max_linear_div_power?(r,rn,y)(m) AND
    max_linear_div_power?(h,hn,y)(kp) AND
    kp>m
    IMPLIES
    (sign_ext(polynomial(p,pn)(x))*sign_ext(polynomial(-r,rn)(x)) = -1 AND
     sign_ext(polynomial(p,pn)(z))*sign_ext(polynomial(-r,rn)(z)) = -1)

  at_zero_remainder_sign_swaps: LEMMA
    FORALL (p,q,h,r:[nat->real],pn,qn,hn,rn:nat):
    x<=y AND y<=z AND
    (FORALL (xyz:real): polynomial(p,pn)(xyz)=
      polynomial(q,qn)(xyz)*polynomial(h,hn)(xyz)
        +polynomial(r,rn)(xyz)) AND
    (FORALL (xyz:real): x<=xyz AND xyz<=z AND
      (polynomial(p,pn)(xyz)=0 OR polynomial(h,hn)(xyz)=0 OR polynomial(r,rn)(xyz)=0)
      IMPLIES xyz = y) AND
   polynomial(h,hn)(y)=0 AND
   polynomial(p,pn)(y)/=0 AND
   polynomial(r,rn)(y)/=0 AND
   polynomial(p,pn)(x)/=0 AND
   polynomial(r,rn)(x)/=0 AND
   polynomial(p,pn)(z)/=0 AND
   polynomial(r,rn)(z)/=0
    IMPLIES
    (sign_ext(polynomial(p,pn)(x))*sign_ext(polynomial(-r,rn)(x)) = -1 AND
     sign_ext(polynomial(p,pn)(z))*sign_ext(polynomial(-r,rn)(z)) = -1)

  %%% All derivatives vanish %%%

  poly_all_derivs_vanish: LEMMA
    (FORALL (i:nat): i<=n IMPLIES polynomial(poly_n_deriv(a,n-i),i)(x)=0)
    IFF
    (FORALL (i:nat): i<=n IMPLIES a(i)=0)


  %%% sign of polynomial values near infinity %%%

  poly_sign_near_infinity: LEMMA a(n)/=0 IMPLIES
    EXISTS (M:posnat): FORALL (x:real): x>=M IMPLIES
      sign_ext(polynomial(a,n)(x)) = sign_ext(a(n))

  poly_sign_near_negative_infinity: LEMMA a(n)/=0 IMPLIES
    EXISTS (M:posnat): FORALL (x:real): x<=-M IMPLIES
      sign_ext(polynomial(a,n)(x)) = sign_ext(IF even?(n) THEN a(n) ELSE -a(n) ENDIF)

  poly_coeff_bound(a,n): RECURSIVE {kr:posreal |
    FORALL (i:nat): i<=n IMPLIES abs(a(i))<kr} =
      IF n = 0 THEN abs(a(0))+1
      ELSE max(abs(a(n))+1,poly_coeff_bound(a,n-1))
      ENDIF MEASURE n
    
  poly_continuity_const(a,n,x,(epsil:posreal)): posreal =
    IF n = 0 THEN 1/2 ELSE 
      LET epcon = epsil/(poly_coeff_bound(a,n) *
                  (sigma(1,n,LAMBDA (i:nat): sigma(1,i,LAMBDA (j:nat): IF (j=0 OR j>i) THEN 0
                ELSE C(i,j-1)*abs(x)^(j-1) ENDIF)) + 1)) 
      IN min(epcon,1/2) 
    ENDIF


  poly_continuity_const_def: LEMMA FORALL (epsil:posreal):
      LET delt = poly_continuity_const(a,n,x,epsil)
      IN  FORALL (y:real): abs(x-y)<delt IMPLIES
         abs(polynomial(a,n)(y)-polynomial(a,n)(x))<epsil

  max_nonvanishing_deriv(a,n,x): 
    RECURSIVE {lastn:nat | lastn <= n AND
            ((EXISTS (ii:upto(n)): a(ii)/=0) 
            IMPLIES (polynomial(poly_n_deriv(a,n-lastn),lastn)(x)/=0 AND
            FORALL (i:nat): i>lastn AND i<=n IMPLIES 
          polynomial(poly_n_deriv(a,n-i),i)(x)=0))} =
    IF n=0 OR polynomial(a,n)(x)/=0 THEN n
    ELSE max_nonvanishing_deriv(poly_deriv(a),n-1,x) ENDIF
    MEASURE n

  poly_rootless_width(a,n,x,(nzb: bool | nzb 
          IFF (EXISTS (i:upto(n)): a(i)/=0))): posreal =
    LET maxn = max_nonvanishing_deriv(a,n,x)
    IN  IF nzb THEN poly_continuity_const(poly_n_deriv(a,n-maxn),maxn,x,
                  abs(polynomial(poly_n_deriv(a,n-maxn),maxn)(x)))
     ELSE 1 ENDIF

  poly_rootless_width_def: LEMMA
    (EXISTS (i:upto(n)): a(i)/=0) IMPLIES
    LET epsil=poly_rootless_width(a,n,x,TRUE),
     mnd  =max_nonvanishing_deriv(a,n,x)
    IN  FORALL (y:real,j:nat): j<=n-mnd 
          AND polynomial(poly_n_deriv(a,j),n-j)(y)=0 AND abs(x-y)<epsil
   IMPLIES x=y

  poly_roots_enumerated: LEMMA (EXISTS (i:upto(n)): a(i)/=0)
    IMPLIES EXISTS (M:nat,rootseq:[below(M)->real]):
      (FORALL (i:below(M)): polynomial(a,n)(rootseq(i))=0)
      AND (FORALL (x:real): polynomial(a,n)(x)=0 IMPLIES
            EXISTS (i:below(M)): x=rootseq(i)) AND injective?(rootseq)

  min_poly_root_distance: LEMMA (EXISTS (i:upto(n)): a(i)/=0)
    IMPLIES EXISTS (epsil:posreal): FORALL (x,y:real):
    polynomial(a,n)(x)=0 AND polynomial(a,n)(y)=0 AND x/=y IMPLIES
    abs(x-y)>=epsil
    
  min_poly_root_dist(a,(n|a(n)/=0)): {epsil:posreal|FORALL (x,y:real):
    polynomial(a,n)(x)=0 AND polynomial(a,n)(y)=0 AND x/=y IMPLIES
    abs(x-y)>epsil}

  % The bound below is very similar to Cauchy's bound.

  poly_root_bound(a,(n|a(n)/=0)): {K:posreal| FORALL (x:real):
    polynomial(a,n)(x)=0 IMPLIES abs(x) < K} =
      max(2,sigma(0,n-1,LAMBDA (i:nat): abs(a(i)))/abs(a(n)) + 1)

  poly_cancel: LEMMA (EXISTS (i:nat):i<=p AND h(i)/=0) AND
    (FORALL (x): polynomial(h,p)(x)*polynomial(a,n)(x) =
           polynomial(h,p)(x)*polynomial(b,m)(x)) IMPLIES
    polynomial(a,n)=polynomial(b,m)

  % In order to make Knuth's bound useful, we need a way to comp kth root.
  % We follow the method of de Moura

  Knuth_bound_simple: LEMMA FORALL (r:real):
    a(n)=1 AND polynomial(a,n)(r)=0 AND r>0 AND n>0 IMPLIES
    EXISTS (k:subrange(1,n)): a(n-k)<0 AND r^k <= - 2^k * a(n-k)

  Knuth_poly_pos_root_bound(a,(n|a(n)=1 AND n>0)): {K:real| FORALL (x:real):
    polynomial(a,n)(x)=0 AND x>0 IMPLIES x <= K} =
      LET maxKfun = (LAMBDA (k:nat): IF 1<=k AND k<=n AND a(n-k)<0
                   THEN LET aquot = -a(n-k),
               log2j = least_pow_2_ge(aquot),
    rootexp = floor(log2j/k)+1
       IN 2^rootexp
                       ELSE -1 ENDIF)
      IN 2*max_rec(maxKfun,1,n)

  Knuth_poly_root_bound(a,(n|a(n)/=0)): {K:nnreal| FORALL (x:real):
    polynomial(a,n)(x)=0 IMPLIES abs(x) <= K} =
      IF n=0 THEN 0
      ELSE
        LET negsign = (LAMBDA (i:nat): IF even?(i) THEN 1 ELSE -1 ENDIF),
     nega = (LAMBDA (i:nat): negsign(i)*negsign(n)*a(i)/a(n)),
     newa = (LAMBDA (i:nat): a(i)/a(n)),
     negbound = Knuth_poly_pos_root_bound(nega,n),
     posbound = Knuth_poly_pos_root_bound(newa,n)
        IN max(posbound,max(negbound,0))
      ENDIF

  Knuth_poly_root_strict_bound(a,(n|a(n)/=0)): {K:posreal| FORALL (x:real):
    polynomial(a,n)(x)=0 IMPLIES abs(x) < K} =
      LET Kprb = Knuth_poly_root_bound(a,n) IN
        IF    Kprb=0 THEN 1
        ELSIF polynomial(a,n)(Kprb)=0 OR polynomial(a,n)(-Kprb)=0 THEN 1.01*Kprb
 ELSE  Kprb ENDIF
     

  poly_increasing_is_strict: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (c:real): xlb <= c AND c <= yub IMPLIES polynomial(poly_deriv(a),n-1)(c) >= 0)
    IFF
    (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) < polynomial(a,n)(y)))

  poly_increasing_is_strict2: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (c:real): xlb <= c AND c <= yub IMPLIES polynomial(poly_deriv(a),n-1)(c) >= 0)
    IFF
    (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) <= polynomial(a,n)(y)))

  poly_decreasing_is_strict: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (c:real): xlb <= c AND c <= yub IMPLIES polynomial(poly_deriv(a),n-1)(c) <= 0)
    IFF
    (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) > polynomial(a,n)(y)))

  poly_decreasing_is_strict2: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (c:real): xlb <= c AND c <= yub IMPLIES polynomial(poly_deriv(a),n-1)(c) <= 0)
    IFF
    (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) >= polynomial(a,n)(y)))

  poly_injective_monotone: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) /= polynomial(a,n)(y))
    IFF
    ((FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) > polynomial(a,n)(y)) OR
     (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) < polynomial(a,n)(y))))

  % Max root is like max_linear_div_power, but more robust.

  root_degree(a,n)(y): RECURSIVE {m| m<=n AND (a(n)/=0 IMPLIES
    ((EXISTS (b:[nat->real]): (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,n-m)(x)) AND
      polynomial(b,n-m)(y)/=0 AND b(n-m)/=0) AND
    (polynomial(a,n)(y)=0 IMPLIES m>0) AND
    ((n>0 AND m>0) IMPLIES (EXISTS (q:[nat->real]): (FORALL (x): polynomial(poly_deriv(a),n-1)(x) = 
             (x-y)^(m-1)*polynomial(q,n-m)(x)) AND
      polynomial(q,n-m)(y)/=0))))} =
    IF polynomial(a,n)(y)/=0 OR n=0 THEN 0
    ELSE 1+root_degree(poly_shift(LAMBDA (i:nat): poly_shift(a,n)(y)(i+1),n-1)(-y),n-1)(y)
    ENDIF MEASURE n

  root_degree_pos: LEMMA a(n)/=0 IMPLIES
    (polynomial(a,n)(y)=0 IFF root_degree(a,n)(y)>0)

  root_degree_max_linear_div_power: LEMMA a(n)/=0 AND
    (polynomial(a,n)(y)=0 OR root_degree(a,n)(y)>0) IMPLIES
     max_linear_div_power?(a,n,y)(root_degree(a,n)(y))

  root_degree_unique: LEMMA
    a(n)/=0 AND m<=n AND (EXISTS (b:[nat->real]): (FORALL (x): 
      polynomial(a,n)(x)=(x-y)^m*polynomial(b,n-m)(x)) AND
      polynomial(b,n-m)(y)/=0) IMPLIES
      m = root_degree(a,n)(y)

  only_root_between?(a,n,x,y)(z): bool =
    x<z AND z<y AND 
    (FORALL (r:real): x<=r AND r<=y AND r/=z IMPLIES
      polynomial(a,n)(r)/=0)

  root_degree_odd: LEMMA a(n)/=0 AND only_root_between?(a,n,x,y)(z) IMPLIES
    (odd?(root_degree(a,n)(z)) IFF sign_ext(polynomial(a,n)(x))=
                 -sign_ext(polynomial(a,n)(y)))

  root_degree_even: LEMMA a(n)/=0 AND only_root_between?(a,n,x,y)(z) IMPLIES
    (even?(root_degree(a,n)(z)) IFF sign_ext(polynomial(a,n)(x))=
                 sign_ext(polynomial(a,n)(y)))

  root_degree_deriv: LEMMA a(n)/=0 AND polynomial(a,n)(y)=0 AND n>0 IMPLIES
    root_degree(poly_deriv(a),n-1)(y) = root_degree(a,n)(y)-1

  root_degree_mult: LEMMA a(n)/=0 AND b(m)/=0 IMPLIES
    root_degree(polynomial_prod(a,n,b,m),n+m)(y) = root_degree(a,n)(y)+root_degree(b,m)(y)

  root_degree_scal: LEMMA a(n)/=0 AND x/=0 IMPLIES
    root_degree(x*a,n)(y) = root_degree(a,n)(y)

  root_degree_power_linear: LEMMA
    root_degree(power_linear(-y, 1, m),m)(y) = m

  root_degree_eq: LEMMA a(n)/=0 AND
    (FORALL (i:upto(n)): a(i)=b(i)) IMPLIES
    root_degree(a,n)(y) = root_degree(b,n)(y)

  root_degree_lower_bound: LEMMA FORALL (k:nat):
    a(n)/=0 AND (EXISTS (b:[nat->real]): b(k)/=0 AND (FORALL (x):
      polynomial(a,n)(x)=(x-y)^m*polynomial(b,k)(x))) IMPLIES
      (k=n-m AND root_degree(a,n)(y)>=m)

  root_degree_division: LEMMA 
    FORALL (a,b,g,h:[nat->real],n,m,k,p:nat):
    (FORALL (x:real): polynomial(a,n)(x) = 
   polynomial(g,k)(x)*polynomial(b,m)(x)
     + polynomial(h,p)(x)) AND h(p)/=0 AND
    a(n)/=0 AND b(m)/=0 IMPLIES
    ((root_degree(a,n)(y)<root_degree(b,m)(y) IMPLIES
      root_degree(h,p)(y)=root_degree(a,n)(y)) AND
     root_degree(h,p)(y)>=
     min(root_degree(a,n)(y),root_degree(b,m)(y)))

  signs_swap_division: LEMMA 
    FORALL (a,b,g,h:[nat->real],n,m,k,p:nat):
    only_root_between?(a,n,x,y)(z) AND
    only_root_between?(b,m,x,y)(z) AND
    only_root_between?(h,p,x,y)(z) AND
    (FORALL (r:real): polynomial(a,n)(r) = 
   polynomial(g,k)(r)*polynomial(b,m)(r)
     + polynomial(h,p)(r)) AND h(p)/=0 AND
    a(n)/=0 AND b(m)/=0 AND
    root_degree(a,n)(z)=root_degree(h,p)(z) AND
    root_degree(b,m)(z)>=root_degree(h,p)(z) IMPLIES
     ((sign_ext(polynomial(a,n)(x))*sign_ext(polynomial(h,p)(x))=1 AND
       sign_ext(polynomial(a,n)(y))*sign_ext(polynomial(h,p)(y))=1) OR
       (EXISTS (sig:Sign): (FORALL (abh:[nat->real],kz:nat): 
         ((abh=a AND kz=n) OR (abh=b AND kz=m) OR (abh=h AND kz=p)) IMPLIES
  sign_ext(polynomial(abh,kz)(x)) = sig*sign_ext(polynomial(abh,kz)(y)))))

END more_polynomial_props