proposition: Lemma algebraic_transform2 : forall (l : IR) (x : nat->IR) (y : nat->IR) (H2 : seq_pos y) (m N1: nat), (( seq_part_sum (fun k : nat => y k [*] (x k [-] l)) (S N1)[+] Sum (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) [=] (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).
proof: Proof. intros. unfold seq_part_sum. apply div_wd. 2: apply eq_reflexive_unfolded. unfold Sum. unfold Sum1. rational. Qed.
imports: CoRN.reals.Series CoRN.reals.PosSeq