proposition: Lemma horner_primitive (c : R) (p : PolR.T) (t : R): PolR.horner tt (PolR.primitive tt c p) t = c + \big[Rplus/0]_(0 <= i < (size p)) (PolR.nth (PolR.primitive tt c p) i.+1 * powerRZ t (Z.of_nat i.+1)).
proof: Proof. rewrite PolR.hornerE PolR.size_primitive big_nat_recl //. congr (_ + _); first by rewrite /= Rmult_1_r. by apply: eq_big_nat => i Hi; rewrite pow_powerRZ. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound