proposition: Lemma partial_sum_null : forall N x, Rseq_pps (fun n => if le_lt_dec n N then 0 else Un n) x N = 0.
proof: Proof. intros N x ; assert (Hrec : forall n, (n <= N)%nat -> Rseq_pps (fun n => if le_lt_dec n N then 0 else Un n) x n = 0). intros n Hn ; induction n. unfold Rseq_pps, gt_pser, Rseq_mult ; simpl ; apply Rmult_0_l. rewrite Rseq_pps_simpl, IHn, Rplus_0_l ; destruct (le_lt_dec (S n) N) as [H | Hf]. apply Rmult_0_l. exfalso ; lia. lia. exfalso ; lia. apply Hrec ; trivial. Qed.
imports: Reals Lra Rsequence Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpser_derivative