let R be domRing; :: thesis: for p being Polynomial of R
for q being non zero Polynomial of R st p divides q holds
deg p <= deg q
let p be Polynomial of R; :: thesis: for q being non zero Polynomial of R st p divides q holds
deg p <= deg q
let q be non zero Polynomial of R; :: thesis: ( p divides q implies deg p <= deg q )
assume p divides q ; :: thesis: deg p <= deg q
then consider r being Polynomial of R such that
A: q = p *' r by RING_4:1;
C: ( p <> 0_. R & r <> 0_. R ) by A;
then reconsider dq = deg q, dr = deg r, dp = deg p as Element of NAT by T8;
dq = dr + dp by A, C, HURWITZ:23;
hence deg p <= deg q by NAT_1:11; :: thesis: verum