for p being Polynomial of F_Real st p <> 0_. F_Real holds
len p = (len (poly_diff p)) + 1