proposition: Lemma root_monic_from_neq0 (p : {poly F}) (x : creal) : p.[x] == 0 -> ((lead_coef p) ^-1 *: p).[x] == 0.
proof: Proof. by rewrite -mul_polyC horner_crealM; move->; rewrite mul_creal0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)