proposition: Lemma sum_N_predN : forall (An:nat -> R) (N:nat), (0 < N)%nat -> sum_f_R0 An N = sum_f_R0 An (pred N) + An N.
proof: Proof. intros. replace N with (S (pred N)). - rewrite tech5. reflexivity. - apply Nat.lt_succ_pred with 0%nat; assumption. Qed.
imports: Rbase Rfunctions Rseries PartSum