theorem lemX: :: FIELD_16:10

for R being Ring
for p1, p2 being Polynomial of R holds p1 *' (- p2) = - (p1 *' p2)