proposition: Lemma partial_sum : forall N x (Vn := fun n : nat => if le_lt_dec n N then 0 else Un n) n (Hle : (N<= n)%nat), Rseq_pps Un x n = Rseq_pps Un x N + Rseq_pps Vn x n.
proof: Proof. intros N x Vn n Hle ; induction Hle. unfold Vn ; rewrite partial_sum_null ; ring. do 2 rewrite Rseq_pps_simpl ; rewrite IHHle ; unfold Vn at 3. destruct (le_lt_dec (S m ) N). exfalso ; lia. apply Rplus_assoc. Qed.
imports: Reals Lra Rsequence Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpser_derivative