theorem prl25: :: RING_5:13

for R being domRing
for p being Polynomial of R
for q being non zero Polynomial of R st p divides q holds
deg p <= deg q