proposition: Lemma horner_coef_creal p x : p.[x] == \big[+%CR/0%:CR]_(i < size p) ((p`_i)%:CR * (x ^+ i))%CR.
proof: Proof. apply: eq_crealP; exists m0=> e n e_gt0 hn /=; rewrite horner_coef. rewrite (@big_morph _ _ (fun u : creal => u n) 0%R +%R) //. rewrite -sumrB /= big1 ?normr0=> //= i _. apply/eqP; rewrite subr_eq0; apply/eqP; congr (_ * _). case: val=> {i} // i; rewrite exprS /exp_creal iteropS. by elim: i=> [|i ihi]; rewrite ?expr0 ?mulr1 //= exprS ihi. 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)