proposition: Lemma Riemann_sum_const (v : V) ptd : Riemann_sum (fun _ => v) ptd = scal (last (SF_h ptd) (SF_lx ptd) - SF_h ptd) v.
proof: Proof. apply SF_cons_ind with (s := ptd) => {ptd} [x0 | [x0 y0] s IH] /=. by rewrite /Riemann_sum /= Rminus_eq_0 scal_zero_l. rewrite Riemann_sum_cons IH /=. rewrite -scal_distr_r /=. apply (f_equal (fun x => scal x v)). rewrite /plus /=. ring. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy