proposition: Lemma size_TM_horner n p Mf (X0 X : I.type) : Pol.size (approx (TM_horner n p Mf X0 X)) = (if 0 < Pol.size p then n else 0).+1.
proof: Proof. rewrite /TM_horner. elim/Pol.poly_ind: p =>[|a p IHp]. by rewrite Pol.fold_polyNil Pol.size_polyNil size_TM_cst. by rewrite Pol.fold_polyCons Pol.size_polyCons size_TM_add size_TM_mul size_TM_cst max1n. 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