proposition: Lemma sum_f_rw (a : nat -> R) (n m : nat) : (n < m)%nat -> sum_f (S n) m a = sum_f_R0 a m - sum_f_R0 a n.
proof: Proof. intro Hnm ; unfold sum_f. revert a n Hnm. induction m ; intros a n Hnm. apply Nat.nlt_0_r in Hnm ; intuition. rewrite (decomp_sum _ _ (Nat.lt_0_succ _)) ; simpl. revert Hnm ; destruct n ; intro Hnm. rewrite Nat.sub_0_r ; simpl ; ring_simplify. clear Hnm IHm. induction m ; simpl. reflexivity. rewrite <- plus_n_Sm, Nat.add_0_r, IHm ; reflexivity. rewrite (decomp_sum _ _ (Nat.lt_0_succ _)) ; simpl ; ring_simplify. apply <-Nat.succ_lt_mono in Hnm. rewrite <- (IHm _ _ Hnm). clear IHm. induction (m - S n)%nat ; simpl. reflexivity. rewrite <- plus_n_Sm, IHn0 ; reflexivity. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)