theorem div100: :: RING_5:21
for R being domRing
for a, b being Element of R holds
( rpoly (1,a) divides rpoly (1,b) iff a = b )