proposition: Theorem cesaro_sum : forall (l : IR) (x : nat -> IR) (H1 : Cauchy_Lim_prop2 x l), Cauchy_Lim_prop2 (fun n : nat => seq_part_sum x (S n) [/]nring (S n)[//](nringS_ap_zero _ n)) l.
proof: Proof. intros. set (y := (fun k : nat => [1] : IR)). assert (H2 : seq_pos y). apply One_seq_is_pos. assert (H3 : seq_inf_sum y). apply One_seq_is_inf_sum. apply Cauchy_Lim_prop2_wd' with (fun n : nat => seq_part_sum (fun k : nat => x k[*] y k) (S n) [/]seq_part_sum y (S n)[//]seq_pos_imp_ap_zero y H2 n). apply cesaro_transform; auto. exists 0. intros. apply div_wd. unfold seq_part_sum. apply Sum0_wd. intros. unfold y. algebra. apply One_part_sum. Qed.
imports: CoRN.reals.Series CoRN.reals.PosSeq