proposition: Lemma Rpser_zip_compat_0_r : forall An x la, Rpser An (x ^ 2) la -> Rpser (Rseq_zip 0 An) x (x * la).
proof: Proof. intros An x la Hla ; replace (x * la) with (0 + x * la) by ring ; apply Rpser_zip_compat ; [apply Rpser_zero_seq | 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