proposition: Lemma Riemann_sum_opp (f : R -> V) ptd : Riemann_sum (fun x => opp (f x)) ptd = opp (Riemann_sum f ptd).
proof: Proof. apply SF_cons_ind with (s := ptd) => {ptd} /= [x0 | [x0 y0] s IH]. rewrite /Riemann_sum /=. rewrite opp_zero //. rewrite !Riemann_sum_cons /= IH. rewrite opp_plus. apply f_equal with (f := fun v => plus v (opp (Riemann_sum f s))). apply scal_opp_r. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy