proposition: Lemma CVU_cv : forall f g c d, CVU f g c d -> forall x, Boule c d x -> Un_cv (fun n => f n x) (g x).
proof: Proof. intros f g c d cvu x bx eps ep; destruct (cvu eps ep) as [N Pn]. exists N; intros n nN; rewrite Rdist_sym; apply Pn; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Ranalysis1 MVT Lra