proposition: Lemma Riemann_sum_minus (f g : R -> V) ptd : Riemann_sum (fun x => minus (f x) (g x)) ptd = minus (Riemann_sum f ptd) (Riemann_sum g ptd).
proof: Proof. unfold minus. rewrite -Riemann_sum_opp. apply Riemann_sum_plus. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy