for f being Polynomial of F_Complex st deg f >= 1 & ex rho being Element of F_Complex st
( Re rho < 0 & |.(eval (f,rho)).| >= |.(eval ((f *'),rho)).| ) holds
not f is Hurwitz by Th49;