proposition: Lemma decomp_sum : forall (An:nat -> R) (N:nat), (0 < N)%nat -> sum_f_R0 An N = An 0%nat + sum_f_R0 (fun i:nat => An (S i)) (pred N).
proof: Proof. intros; induction N as [| N HrecN]. - elim (Nat.lt_irrefl _ H). - cut ((0 < N)%nat \/ N = 0%nat). + intro; elim H0; intro. * cut (S (pred N) = pred (S N)). -- intro; rewrite <- H2. do 2 rewrite tech5. replace (S (S (pred N))) with (S N). ++ rewrite (HrecN H1); ring. ++ rewrite H2; simpl; reflexivity. -- destruct (O_or_S N) as [(m,<-)|<-]. ++ simpl; reflexivity. ++ elim (Nat.lt_irrefl _ H1). * rewrite H1; simpl; reflexivity. + inversion H. * right; reflexivity. * left; apply Nat.lt_le_trans with 1%nat; [ apply Nat.lt_0_succ | assumption ]. Qed.
imports: Rbase Rfunctions Rseries Rcomplete