proposition: Lemma Riemann_sum_cons (f : R -> V) (h0 : R * R) (ptd : SF_seq) : Riemann_sum f (SF_cons h0 ptd) = plus (scal (SF_h ptd - fst h0) (f (snd h0))) (Riemann_sum f ptd).
proof: Proof. rewrite /Riemann_sum /=. case: h0 => x0 y0 ; apply SF_cons_dec with (s := ptd) => {ptd} [ x1 | [x1 y1] ptd ] //=. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy