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