proposition: Lemma Rpol_integral_0 (x1 x2 : R) (p : PolR.T) : RInt (PolR.horner tt p) x1 x2 = PolR.horner tt (PolR.primitive tt 0 p) x2 - PolR.horner tt (PolR.primitive tt 0 p) x1.
proof: Proof. apply is_RInt_unique. apply: (is_RInt_ext (Derive (PolR.horner tt (PolR.primitive tt R0 p)))). by move => x _; rewrite Rpol_derive. apply: is_RInt_derive. move => x _; apply: Derive_correct; apply: PolR.ex_derive_horner. move => x _. apply: (continuous_ext (PolR.horner tt p) ) => [t|] . by rewrite Rpol_derive. exact: Rpol_continuous. 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