:: deftheorem defines with_negative_coefficients HURWITZ2:def 12 :
for p being real Polynomial of F_Complex holds
( p is with_negative_coefficients iff for i being Nat st i <= deg p holds
p . i < 0 );