for a, b being Element of F_Complex st |.a.| > |.b.| holds
for f being Polynomial of F_Complex st deg f >= 1 holds
( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz )