fact: Definition TM_horner n p (Mf : rpa) (X0 X : I.type) : rpa := @Pol.fold rpa (fun a b => (TM_add (TM_cst X a) (TM_mul b Mf X0 X n))) (TM_cst X I.zero) p.
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