proposition: Lemma Pser_Rpser_link : forall An x l, Pser An x l <-> Rpser An x l.
proof: Proof. intros An x l ; split ; intro Hyp ; apply Hyp. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR