proposition: Lemma RInt_comp (f : R -> V) (g dg : R -> R) (a b : R) : (forall x, Rmin a b <= x <= Rmax a b -> continuous f (g x)) -> (forall x, Rmin a b <= x <= Rmax a b -> is_derive g x (dg x) /\ continuous dg x) -> RInt (fun y => scal (dg y) (f (g y))) a b = RInt f (g a) (g b).
proof: Proof. move => Hfg Hg. have H := (is_RInt_comp _ _ _ _ _ Hfg Hg). exact: is_RInt_unique. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(eqtype seq) Markov Rcomplements Rbar Lub Lim_seq Derive SF_seq Continuity Hierarchy Seq_fct RInt PSeries