proposition: Lemma is_RInt_translation_sub V g x a b Ig : @is_RInt V g (a - x) (b - x) Ig -> is_RInt (fun y : R => g (y - x)) a b Ig.
proof: Proof. exact: is_RInt_translation_add. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp