deg (Leading-Monomial p) = deg p by POLYNOM4:15;
hence deg (Leading-Monomial p) <= 0 by RATFUNC1:def 2; :: according to RATFUNC1:def 2 :: thesis: verum