proposition: Lemma CVU_CVS_dom (fn : nat -> R -> R) (D : R -> Prop) : CVU_dom fn D -> CVS_dom fn D.
proof: Proof. move => Hcvu x Hx. exists (real (Lim_seq (fun n => fn n x))). apply is_lim_seq_spec. intros eps. case: (Hcvu eps) => {Hcvu} N Hcvu. exists N => n Hn. by apply Hcvu. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Continuity Derive Series Lub Hierarchy