proposition: Lemma CVU_dom_include (fn : nat -> R -> R) (D1 D2 : R -> Prop) : (forall y, D2 y -> D1 y) -> CVU_dom fn D1 -> CVU_dom fn D2.
proof: Proof. move => H H1 eps. case: (H1 eps) => {H1} N H1. exists N => n Hn x Hx. apply H1. exact Hn. by apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Continuity Derive Series Lub Hierarchy