proposition: Lemma Riemann_sum_plus (f g : R -> V) ptd : Riemann_sum (fun x => plus (f x) (g x)) ptd = plus (Riemann_sum f ptd) (Riemann_sum g ptd).
proof: Proof. apply SF_cons_ind with (s := ptd) => {ptd} /= [x0 | [x0 y0] s IH]. rewrite /Riemann_sum /=. apply sym_eq, @plus_zero_l. rewrite !Riemann_sum_cons /= ; rewrite IH. rewrite scal_distr_l. rewrite -!plus_assoc. apply f_equal. rewrite !plus_assoc. apply (f_equal (fun x => plus x (Riemann_sum g s))). apply plus_comm. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy