proposition: Lemma Rpol_continuous p (x : R) : continuous (PolR.horner tt p) x.
proof: Proof. have Hext : forall t, foldr (fun a b => (b * t) + a) 0 (PolR.toSeq p) = PolR.horner tt p t => [t|]. by rewrite PolR.horner_seq. apply: (continuous_ext _ _ _ Hext). elim: (PolR.toSeq p) => [|a q HI] /=. - exact: continuous_const. - apply: continuous_plus; last by exact: continuous_const. by apply: continuous_mult => //; exact: continuous_id. 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