proposition: Lemma pol_int_sub pol x1 x2 x3 : ex_RInt (fun y : R => pol.[y - x3]) x1 x2.
proof: Proof. have -> : x1 = x1 - x3 + x3 by ring. have -> : x2 = x2 - x3 + x3 by ring. apply: ex_RInt_translation_sub. exact: Rpol_integrable. 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