proposition: Lemma Rpser_zero_seq : forall (x : R), Rpser (zero_seq) x 0.
proof: Proof. intros x eps eps_pos ; exists O ; intros n _ ; unfold R_dist ; apply Rle_lt_trans with (Rabs 0) ; [right ; apply Rabs_eq_compat | rewrite Rabs_R0 ; assumption]. unfold Rminus ; rewrite Ropp_0, Rplus_0_r ; induction n ; simpl ; [| rewrite Rseq_pps_simpl, IHn] ; unfold Rseq_pps, zero_seq, Rseq_constant, gt_pser, Rseq_mult ; simpl ; ring. 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