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

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