proposition: Lemma Riemann_sum_compat f (s : SF_seq) (pr : SF_sorted Rle s) : Riemann_sum f s = RiemannInt_SF (SF_compat_le (SF_map f s) (SF_map_sort f s _ pr)).
proof: Proof. rewrite /RiemannInt_SF ; case: Rle_dec => // [_ | H]. move: pr ; apply SF_cons_ind with (s := s) => {s} [x0 | h s IH] pr //=. rewrite /= -IH /Riemann_sum /SF_map /= => {IH}. rewrite Rmult_comm. by apply SF_cons_dec with (s := s). apply pr. contradict H ; rewrite -nth_last -nth0 ; move: (Nat.le_refl (ssrnat.predn (size (SF_lx (SF_map f s))))) ; elim: {1 3}(ssrnat.predn (size (SF_lx (SF_map f s)))) => /= [| i IH] Hi. apply Rle_refl. apply Rle_trans with (1 := IH (Nat.le_trans _ _ _ (Nat.le_succ_diag_r i) Hi)), (sorted_nth Rle) ; intuition. by apply SF_map_sort. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy