proposition: Lemma Riemann_sum_rcons (f : R -> V) ptd l0 : Riemann_sum f (SF_rcons ptd l0) = plus (Riemann_sum f ptd) (scal (fst l0 - last (SF_h ptd) (SF_lx ptd)) (f (snd l0))).
proof: Proof. rewrite /Riemann_sum . case: l0 => x0 y0. apply SF_rcons_dec with (s := ptd) => {ptd} [ x1 | ptd [x1 y1]]. apply plus_comm. rewrite ?SF_map_rcons /=. rewrite pairmap_rcons foldr_rcons /=. rewrite unzip1_rcons last_rcons /=. set l := pairmap _ _ _. induction l ; simpl. apply plus_comm. rewrite IHl. apply plus_assoc. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy