proposition: Lemma Riemann_sum_map (f : R -> V) (g : R -> R) ptd : Riemann_sum (fun x => f (g x)) ptd = Riemann_sum f (SF_map g ptd).
proof: Proof. apply SF_cons_ind with (s := ptd) => {ptd} [x0 | h ptd IH]. by []. rewrite SF_map_cons !Riemann_sum_cons /=. by rewrite IH. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy