proposition: Lemma sum_f_to_big n (f : nat -> R) : sum_f_R0 f n = \big[Rplus/0%R]_(0 <= i < n.+1) f i.
proof: Proof. elim: n =>[|n IHn]; first by rewrite big_nat_recl // big_mkord big_ord0 Rplus_0_r. by rewrite big_nat_recr //= IHn. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor