proposition: Lemma One_seq_is_inf_sum : seq_inf_sum (fun n : nat => [1]).
proof: Proof. unfold seq_inf_sum. intros. assert ({N : nat | M [<] nring N}). apply Archimedes'. destruct X as [N H]. exists N. intros. apply less_leEq_trans with (nring (R:=IR) N); auto. assert (seq_part_sum (fun n : nat => [1]) m [=] nring m). apply One_part_sum. astepr (nring (R:=IR) m). apply nring_leEq. auto. Qed.
imports: CoRN.reals.Series