for p being Polynomial of F_Real holds poly_diff (Leading-Monomial p) = (0_. F_Real) +* (((len p) -' 2),((p . ((len p) -' 1)) * ((len p) -' 1)))