proposition: Lemma Riemann_sum_scal (a : R) (f : R -> V) ptd : Riemann_sum (fun x => scal a (f x)) ptd = scal a (Riemann_sum f ptd).
proof: Proof. apply SF_cons_ind with (s := ptd) => {ptd} /= [x0 | [x0 y0] s IH]. rewrite /Riemann_sum /=. apply sym_eq. apply @scal_zero_r. rewrite !Riemann_sum_cons /= IH. rewrite scal_distr_l. apply f_equal with (f := fun v => plus v _). rewrite 2!scal_assoc. by rewrite /mult /= Rmult_comm. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy