theorem degA: :: RING_2:29

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