proposition: Lemma Riemann_sum_pair {U : ModuleSpace R_Ring} {V : ModuleSpace R_Ring} (f : R -> U * V) ptd : Riemann_sum f ptd = (Riemann_sum (fun t => fst (f t)) ptd, Riemann_sum (fun t => snd (f t)) ptd).
proof: Proof. apply SF_cons_ind with (s := ptd) => {ptd} [x0 | h0 ptd IH]. by []. rewrite !Riemann_sum_cons IH. by apply injective_projections. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy