proposition: Lemma nonneg_poly_deg2 (z : C) : nonneg ('X^2 + (1 *- 2 * Re z) *: 'X + (Re z ^+ 2 + Im z ^+ 2)%:P) = ((Re z) <= 0).
proof: Proof. rewrite -(mul1r 'X^2) mul_polyC polyseq_deg2 /= ?oner_neq0 // ler01 !andbT. by rewrite nmulr_rge0 ?oppr_lt0 ?ltr0n // addr_ge0 // sqr_ge0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol