theorem divmod: :: FIELD_5:16

for F being Field
for p being Polynomial of F
for q being non zero Polynomial of F holds deg (p mod q) < deg q