proposition: Lemma diff_is_sum : forall (s : nat -> IR) N m, N < m -> s m[-]s N [=] Sum N (pred m) (fun i => s (S i) [-]s i).
proof: Proof. intros s N m ltNm. unfold Sum in |- *. unfold Sum1 in |- *. generalize (Nat.lt_succ_pred N m ltNm). intro H. symmetry in H. rewrite <- H. generalize (diff_is_Sum0 s N). intro HsN. generalize (diff_is_Sum0 s m). intro Hsm. apply eq_transitive_unfolded with (s m[-]s 0[-] (s N[-]s 0)). rational. apply (cg_minus_wd IR). assumption. assumption. Qed.
imports: CoRN.reals.CReals1