proposition: Lemma RInt_val_Reals (f : R -> R) (a b : R) (n : nat) : RInt_val f a b n = RiemannInt_SF (sf_SF_val_fun f a b n).
proof: Proof. rewrite /RiemannInt_SF SF_val_subdiv SF_val_subdiv_val ; case: Rle_dec => Hab. rewrite /RInt_val /SF_val_ly ; case: (unif_part a b n) => [| h s] /=. by []. elim: s h => [|h0 s IH] h /=. by []. rewrite (SF_cons_f2 _ h). 2: by apply Nat.lt_0_succ. rewrite Riemann_sum_cons /= IH /plus /scal /= /mult /=. ring. rewrite RInt_val_swap /SF_val_ly /RInt_val. simpl opp ; apply f_equal. case: (unif_part b a n) => [| h s] /=. by []. elim: s h => [|h0 s IH] h /=. by []. rewrite SF_cons_f2. 2: by apply Nat.lt_0_succ. rewrite Riemann_sum_cons IH /= /plus /scal /= /mult /=. ring. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy