proposition: Lemma Riemann_sum_zero (f : R -> V) ptd : SF_sorted Rle ptd -> SF_h ptd = last (SF_h ptd) (SF_lx ptd) -> Riemann_sum f ptd = zero.
proof: Proof. apply SF_cons_ind with (s := ptd) => {ptd} [x0 | [x0 y0] ptd IH] //= Hs Hhl. rewrite Riemann_sum_cons IH /= => {IH}. replace x0 with (SF_h ptd). rewrite Rminus_eq_0. rewrite plus_zero_r. by apply: scal_zero_l. apply Rle_antisym. rewrite Hhl => {Hhl} /=. apply (sorted_last (SF_h ptd :: @map (R*R) R (@fst R R) (SF_t ptd)) O) with (x0 := 0). replace ((SF_h ptd) :: map _ _) with (SF_lx ptd). apply Hs. apply SF_cons_ind with (s := ptd) => {ptd Hs} [x1 | [x1 y1] ptd IH] //=. apply Nat.lt_0_succ. apply Hs. apply Hs. apply Rle_antisym. apply (sorted_last (SF_h ptd :: @map (R*R) R (@fst R R) (SF_t ptd)) O) with (x0 := 0). replace ((SF_h ptd) :: map _ _) with (SF_lx ptd). apply Hs. apply SF_cons_ind with (s := ptd) => {ptd Hs Hhl} [x1 | [x1 y1] ptd IH] //=. apply Nat.lt_0_succ. move: Hhl ; rewrite -?(last_map (@fst R R)) /= => <- ; apply Hs. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy