theorem Th44: :: POLYDIFF:44
for p being Polynomial of F_Real st p <> 0_. F_Real holds
len (poly_diff p) = (len p) - 1