proposition: Lemma horner_pi (p : {poly F}) (x : algcreal) : (p ^ to_alg).[\pi_alg x] = \pi (horner_algcreal p x).
proof: Proof. rewrite horner_coef /horner_algcreal size_map_poly. apply: (big_ind2 (fun x y => x = \pi_alg y)). + by rewrite zeroE. + by move=> u u' v v' -> ->; rewrite [_ + _]piE. by move=> i /= _; rewrite expn_pi coef_map /= [_ * _]piE. Qed.
imports: HB(structures) 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 generic_quotient) mathcomp(cauchyreals separable zmodp bigenough)