proposition: Lemma diff_is_Sum0 : forall (s : nat -> IR) n, s n[-]s 0 [=] Sum0 n (fun i => s (S i) [-]s i).
proof: Proof. intros s. simple induction n. simpl in |- *. algebra. intros. simpl in |- *. apply eq_transitive_unfolded with (s (S n0) [-]s n0[+] (s n0[-]s 0)). rational. apply eq_transitive_unfolded with (s (S n0) [-]s n0[+]Sum0 n0 (fun i : nat => s (S i) [-]s i)). exact (plus_resp_eq _ _ _ _ H). rational. Qed.
imports: CoRN.reals.CReals1