for p being non constant real with_positive_coefficients Polynomial of F_Complex st [(even_part p),(odd_part p)] is one_port_function & degree [(even_part p),(odd_part p)] = degree p holds
p is Hurwitz