proposition: Lemma sum_f_u_add (u : nat -> R) (p n m : nat) : (n <= m)%nat -> sum_f (n + p)%nat (m + p)%nat u = sum_f n m (fun k => u (k + p)%nat).
proof: Proof. move => H ; rewrite /sum_f. rewrite ?(Nat.add_comm _ p) -MyNat.add_sub_add_l. elim: (m - n)%nat => [ | k IH] //=. by rewrite Nat.add_comm. rewrite IH ; repeat apply f_equal. ring. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)