proposition: Lemma seq_inf_sum_ratio_bound : forall (y : nat->IR) (H2 : seq_pos y) (m N1: nat) (H3: S N1 < m), AbsSmall [1] (Sum (G:=IR) (S N1) m (fun k : nat => y k)[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m).
proof: Proof. intros. apply leEq_imp_AbsSmall. apply shift_leEq_div. apply seq_pos_imp_sum_pos; auto. astepl ([0]:IR). apply less_leEq. apply seq_pos_imp_sum_pos'; auto. apply shift_div_leEq. apply seq_pos_imp_sum_pos; auto. astepl (Sum (G:=IR) (S N1) m y). astepr (seq_part_sum y (S m)). unfold Sum. unfold Sum1. unfold seq_part_sum. apply shift_zero_leEq_minus'. rstepr (Sum0 (G:=IR) (S N1) y). apply less_leEq. astepr (seq_part_sum y (S N1)). apply seq_pos_imp_sum_pos; auto. Qed.
imports: CoRN.reals.Series