proposition: Lemma is_RInt_translation_add V g a b x Ig : @is_RInt V g (a + x) (b + x) Ig -> is_RInt (fun y : R => g (y + x)%R) a b Ig.
proof: Proof. have -> : a + x = (1 * a + x) by rewrite Rmult_1_l. have -> : b + x = (1 * b + x) by rewrite Rmult_1_l. move /is_RInt_comp_lin. apply: is_RInt_ext => t. now rewrite Rmult_1_l scal_one. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp