proposition: Lemma monic_roots_changes_eq0 (p : {poly R}) : p \is monic -> (forall (z : C), (root (toC p) z) -> (Re z <= 0)) -> changes p = 0%N.
proof: Proof. move=> Hpmonic H. by rewrite nonneg_changes0 // nonneg_root_nonpos. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol