proposition: Lemma RInt_translation_add V g a b x : ex_RInt g (a + x) (b + x) -> @RInt V (fun y : R => g (y + x)%R) a b = RInt g (a + x) (b + x).
proof: Proof. intros HI. apply is_RInt_unique. apply is_RInt_translation_add. exact: RInt_correct. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp