proposition: Lemma sum_f_R0_skip (u : nat -> R) (n : nat) : sum_f_R0 (fun k => u (n - k)%nat) n = sum_f_R0 u n.
proof: Proof. suff H : forall n m, (n < m)%nat -> sum_f n m (fun k => u ((m - k) + n)%nat) = sum_f n m u. case: n => [ | n] //. move: (H _ _ (Nat.lt_0_succ n)) => {} H. rewrite /sum_f in H. transitivity (sum_f_R0 (fun x : nat => u (S n - (x + 0) + 0)%nat) (S n - 0)). replace (S n - 0)%nat with (S n) by auto. elim: {2 4}(S n) => [ | m IH] //. simpl ; by rewrite Nat.add_0_r. rewrite /sum_f_R0 -/sum_f_R0 -IH. apply f_equal. by rewrite ?Nat.add_0_r. rewrite H. replace (S n - 0)%nat with (S n) by auto. elim: (S n) => [ | m IH] //. rewrite /sum_f_R0 -/sum_f_R0 -IH. apply f_equal. by rewrite Nat.add_0_r. move => {} n m H. elim: m u H => [ | m IH] u H //. apply (proj1 (Nat.lt_succ_r _ _)), le_lt_eq_dec in H ; case: H IH => [H IH | -> _ {n}] //. rewrite sum_f_n_Sm ; try by intuition. replace (sum_f n (S m) u) with (sum_f n (S m) u - u n + u n) by ring. rewrite -sum_f_Sn_m ; try by intuition. rewrite sum_f_u_Sk ; try by intuition. rewrite -(IH (fun k => u (S k))) => {IH} ; try by intuition. apply f_equal2. rewrite /sum_f. elim: {1 3 4}(m - n)%nat (Nat.le_refl (m-n)%nat) => [ | k IH] // Hk ; rewrite /sum_f_R0 -/sum_f_R0. apply f_equal. rewrite Nat.add_0_l MyNat.sub_add ; intuition. rewrite IH ; try by intuition. by rewrite Nat.sub_diag Nat.add_0_l. rewrite /sum_f. rewrite Nat.sub_succ_l ; try by intuition. rewrite Nat.sub_diag. rewrite /sum_f_R0 -/sum_f_R0. replace (1+m)%nat with (S m) by ring. rewrite Nat.add_0_l Nat.sub_diag MyNat.sub_add ; intuition. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)