proposition: Lemma algebraic_estimate1 : forall (e l: IR) (H1 : [0] [<] e) (x : nat -> IR) (y : nat->IR) (H2 : seq_pos y) (m N1: nat) (H3 : S N1 <= m) (H4 : forall i, S N1 <= i -> i <= m -> AbsSmall e (x i[-]l)), AbsSmall (Sum (G:=IR) (S N1) m (fun k : nat => y k[*]e)[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m) (Sum (G:=IR) (S N1) m (fun k : nat => y k[*](x k[-]l))[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m).
proof: Proof. intros. apply AbsSmall_cancel_mult with (seq_part_sum y (S m)). apply seq_pos_imp_sum_pos; auto. astepl (Sum (G:=IR) (S N1) m (fun k : nat => y k[*]e)). astepr (Sum (G:=IR) (S N1) m (fun k : nat => y k[*](x k[-]l))). apply sum_resp_AbsSmall; auto. intros. apply mult_resp_AbsSmall. apply less_leEq. apply H2. apply H4; auto. Qed.
imports: CoRN.reals.Series CoRN.reals.PosSeq