proposition: Lemma eval_Horner e p x : eval e (Horner p x) = (eval_poly e p).[eval e x].
proof: Proof. by elim: p => /= [|a p ihp]; rewrite !(horner0, hornerE) // ihp. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)