proposition: Lemma CVU_ext_lim : forall f g1 g2 c d, CVU f g1 c d -> (forall x, Boule c d x -> g1 x = g2 x) -> CVU f g2 c d.
proof: Proof. intros f g1 g2 c d cvu q eps ep; destruct (cvu _ ep) as [N Pn]. exists N; intros; rewrite <- q; auto. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra