proposition: Lemma ge_cauchy_bound p : p != 0 -> {in `[cauchy_bound p, +oo[, noroot p}.
proof: Proof. move=> p_neq0 x; rewrite in_itv andbT /=; apply/contra_leN. by case/rootP/(cauchy_boundP p_neq0)/ltr_normlP; rewrite ltr_oppl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)