proposition: Lemma sum_f_R0_sumR : forall n (f : nat -> R), sum_f_R0 f n = \sum_(i < n.+1) f i.
proof: Proof. elim => [f|n IH f] /=; first by rewrite big_ord_recl /= big_ord0 addR0. by rewrite big_ord_recr /= IH. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)