proposition: Lemma sum_f_u_Sk (u : nat -> R) (n m : nat) : (n <= m)%nat -> sum_f (S n) (S m) u = sum_f n m (fun k => u (S k)).
proof: Proof. move => H ; rewrite /sum_f. simpl minus. elim: (m - n)%nat => [ | k IH] //=. rewrite IH ; repeat apply f_equal. by rewrite plus_n_Sm. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)