for p, q being Polynomial of F_Real holds poly_diff (p + q) = (poly_diff p) + (poly_diff q)