proposition: Lemma seq_pos_imp_sum_pos : forall (x : nat -> IR), seq_pos x -> forall n, [0] [<] seq_part_sum x (S n).
proof: Proof. intros. induction n. simpl. astepl ([0][+][0]:IR). apply plus_resp_less_lft. apply X. simpl. simpl in |- *. apply plus_resp_pos. apply IHn. apply X. Qed.
imports: CoRN.reals.Series