proposition: Lemma seq_inf_sum_imp_div_small : forall (x : nat -> IR) (H1 : seq_inf_sum x) (H2: seq_pos x) (C e : IR) (H4 : [0] [<] e), { N : nat | forall m : nat, N <= m -> AbsSmall e (C [/](seq_part_sum x (S m)) [//] (seq_pos_imp_ap_zero x H2 m))}.
proof: Proof. unfold seq_inf_sum. unfold seq_pos. intros. assert ({N : nat | forall m : nat, N <= m -> ((AbsIR C)[/]e[//]pos_ap_zero IR e H4)[<]seq_part_sum x m}). apply (H1 ((AbsIR C) [/] e [//] (pos_ap_zero IR e H4))). destruct X as [N H]. exists N. intros. assert (H3 : ((AbsIR C)[/]e[//]pos_ap_zero IR e H4)[<]seq_part_sum x (S m)). apply H; auto. astepr ((C [/] seq_part_sum x (S m)[//] (seq_pos_imp_ap_zero x H2 m))). assert (AbsSmall ((seq_part_sum x (S m))[*]e) C). apply AbsIR_imp_AbsSmall. apply less_leEq. apply (shift_less_mult IR (AbsIR C) (seq_part_sum x (S m)) e (pos_ap_zero IR e H4)); auto. rstepl ((seq_part_sum x (S m))[*]e [/] (seq_part_sum x (S m))[//] pos_ap_zero IR (seq_part_sum x (S m)) (seq_pos_imp_sum_pos x H2 m)). rstepr (C [/] (seq_part_sum x (S m))[//] pos_ap_zero IR (seq_part_sum x (S m)) (seq_pos_imp_sum_pos x H2 m)). apply div_resp_AbsSmall. auto. Qed.
imports: CoRN.reals.Series