proposition: Lemma root_poly_expn_creal p k x : (0 < k)%N -> (p ^+ k).[x] == 0 -> p.[x] == 0.
proof: Proof. move=> k_gt0 pkx_eq0; apply: eq_crealP; exists_big_modulus m F. move=> e i e_gt0 hi; rewrite /= subr0. rewrite -(@ltr_pexpn2r _ k) -?topredE /= ?normr_ge0 ?ltW //. by rewrite -normrX -horner_exp (@eq0_modP _ pkx_eq0) ?exprn_gt0 //. by close. 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)