theorem div1: :: RING_4:2

for F being Field
for p, q being Polynomial of F st deg p < deg q holds
p mod q = p