proposition: Lemma Un_cv_ext : forall un vn, (forall n, un n = vn n) -> forall l, Un_cv un l -> Un_cv vn l.
proof: Proof. intros un vn quv l P eps ep; destruct (P eps ep) as [N Pn]; exists N. intro n; rewrite <- quv; apply Pn. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia