proposition: Lemma seq_pos_imp_ap_zero : forall (x : nat -> IR), seq_pos x -> forall n, seq_part_sum x (S n) [#] [0].
proof: Proof. unfold seq_pos. intros. apply ap_symmetric_unfolded. apply less_imp_ap. apply seq_pos_imp_sum_pos; auto. Qed.
imports: CoRN.reals.Series