proposition: Lemma algebraic_transform3: forall (eps: IR) (y : nat->IR) (H2 : seq_pos y) (m N1: nat), (eps[/]TwoNZ [*] (Sum (S N1) m (fun k: nat => y k)[/] 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[*]eps [/]TwoNZ)[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m).
proof: Proof. intros. astepl ((eps[/]TwoNZ [*] (Sum (S N1) m (fun k: nat => y k)))[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m). astepr (Sum (G:=IR) (S N1) m (fun k : nat => eps[/]TwoNZ[*]y k)[/] seq_part_sum y (S m)[//]seq_pos_imp_ap_zero y H2 m). apply div_wd. 2: apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. astepr (eps[/]TwoNZ[*]Sum (G:=IR) (S N1) m y). apply mult_distr_sum_lft. Qed.
imports: CoRN.reals.Series CoRN.reals.PosSeq