theorem div4: :: RING_4:5

for F being Field
for p, r being Polynomial of F
for q being non zero Polynomial of F holds
( (p + r) div q = (p div q) + (r div q) & (p + r) mod q = (p mod q) + (r mod q) )