proposition: Lemma Pser_constant_seq : forall (r : R) (x : R), Pser (constant_seq r) x r.
proof: Proof. intros r x. assert (Hrew : forall n, sum_f_R0 (fun n => (constant_seq r) n * x ^ n) n = r). induction n. unfold constant_seq ; simpl ; apply Rmult_1_r. simpl ; rewrite IHn ; unfold constant_seq ; simpl ; rewrite Rmult_0_l, Rplus_0_r ; reflexivity. intros eps eps_pos ; exists O ; intros n n_lb ; rewrite Hrew, R_dist_eq ; assumption. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity