proposition: Lemma sum_f_n_Sm (u : nat -> R) (n m : nat) : (n <= m)%nat -> sum_f n (S m) u = sum_f n m u + u (S m).
proof: Proof. move => H. rewrite /sum_f Nat.sub_succ_l // /sum_f_R0 -/sum_f_R0. rewrite plus_Sn_m. by rewrite MyNat.sub_add. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)