proposition: Lemma algebraic_transform1 : forall (l : IR) (x : nat->IR) (y : nat->IR) (H2 : seq_pos y) (m : nat), (seq_part_sum (fun k : nat => y k [*] (x k [-] l)) (S m)[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m) [=] ((seq_part_sum (fun k : nat => x k[*]y k) (S m)[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m)[-]l).
proof: Proof. intros. rstepr (((seq_part_sum (fun k : nat => x k[*]y k) (S m))[-] l[*](seq_part_sum y (S m)))[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m). apply div_wd. 2: apply eq_reflexive_unfolded. unfold seq_part_sum. unfold cg_minus. astepr (Sum0 (G:=IR) (S m) (fun k : nat => x k[*]y k)[+] Sum0 (G:=IR) (S m) (fun k : nat => [--]l[*]y k)). astepr (Sum0 (G:=IR) (S m) (fun k : nat => x k[*]y k[+][--]l[*]y k)). apply Sum0_wd. intros. rational. apply (Sum0_plus_Sum0 IR (fun k : nat => x k [*] y k) (fun k : nat => [--] l [*] y k) (S m)). apply plus_resp_eq. astepr ([--]l [*] (Sum0 (G:=IR) (S m) y)). apply mult_distr_sum0_lft. Qed.
imports: CoRN.reals.Series CoRN.reals.PosSeq