proposition: Lemma Pser_ext : forall x l, Pser An x l <-> Pser Bn x l.
proof: Proof. intros x l ; split ; intros HP eps eps_pos ; destruct (HP _ eps_pos) as [N HN] ; exists N ; intros n n_lb ; [rewrite (sum_eq _ (fun n => An n * x ^ n)%R) | rewrite (sum_eq _ (fun n => Bn n * x ^ n)%R)] ; ((apply HN ; assumption) || (intros ; rewrite AnBn_ext ; reflexivity)). Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_sums Rpser_cv_facts Rinterval Ranalysis_def Rfunction_facts Tactics