proposition: Lemma ex_RInt_translation_add V g x a b : @ex_RInt V g a b -> @ex_RInt V (fun t => g (t + x)) (a - x) (b - x).
proof: Proof. intros [Ig HI]. exists Ig. apply: is_RInt_translation_add. by rewrite 2!Rplus_assoc Rplus_opp_l 2!Rplus_0_r. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp