proposition: Lemma seq_pos_imp_sum_pos' : forall (x : nat -> IR) (H1 : seq_pos x) (n m : nat) (H2 : m < n), [0] [<] Sum m n x.
proof: Proof. unfold seq_pos. intros. induction n. assert (~ m < 0). auto with arith. contradiction. elim (le_lt_eq_dec _ _ H2); intros H3. astepr (Sum m n x [+] x (S n)). apply plus_resp_pos. apply IHn; auto with arith. apply H1. replace n with m; auto. astepr (Sum m m x [+]x (S m)). apply plus_resp_pos. astepr (x m). apply H1. apply H1. Qed.
imports: CoRN.reals.Series