theorem div5: :: RING_4:4

for F being Field
for p, q being Polynomial of F holds p = ((p div q) *' q) + (p mod q)