p <> 0_. L ;
then deg p <> - 1 by HURWITZ:20;
then len p <> 0 ;
then (deg p) + 1 > 0 ;
then deg p in NAT by INT_1:3, INT_1:7;
hence degree p is natural ; :: thesis: verum