proposition: Lemma sum_f_Sn_m (u : nat -> R) (n m : nat) : (n < m)%nat -> sum_f (S n) m u = sum_f n m u - u n.
proof: Proof. move => H. elim: m n H => [ | m IH] // n H. by apply Nat.nlt_0_r in H. rewrite sum_f_u_Sk ; try by intuition. rewrite sum_f_n_Sm ; try by intuition. replace (sum_f n m u + u (S m) - u n) with ((sum_f n m u - u n) + u (S m)) by ring. apply (proj1 (Nat.lt_succ_r _ _)), le_lt_eq_dec in H. case: H => [ H | -> {n} ] //. rewrite -IH => //. rewrite /sum_f ; simpl. rewrite MyNat.sub_succ_r. apply lt_minus_O_lt in H. rewrite -{3}(MyNat.sub_add n m) ; try by intuition. case: (m-n)%nat H => {IH} [ | k] //= H. by apply Nat.nlt_0_r in H. apply (f_equal (fun y => y + _)). elim: k {H} => [ | k IH] //. rewrite /sum_f_R0 -/sum_f_R0 IH ; repeat apply f_equal ; intuition. rewrite /sum_f Nat.sub_diag /= ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)