proposition: Lemma RInt_val_point (f : R -> V) (a : R) (n : nat) : RInt_val f a a n = zero.
proof: Proof. unfold RInt_val ; apply Riemann_sum_zero. rewrite /SF_sorted SF_lx_f2. apply unif_part_sort ; apply Rle_refl. rewrite size_mkseq ; by apply Nat.lt_0_succ. rewrite SF_lx_f2 /=. rewrite -{2}[1]/(INR 1) last_map. unfold Rdiv ; ring. by apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy