proposition: Lemma cond_pos_sum : forall (An:nat -> R) (N:nat), (forall n:nat, 0 <= An n) -> 0 <= sum_f_R0 An N.
proof: Proof. intros. induction N as [| N HrecN]. - simpl; apply H. - rewrite tech5. apply Rplus_le_le_0_compat. + apply HrecN. + apply H. Qed.
imports: Rbase Rfunctions Rseries Rcomplete