proposition: Lemma Un_cv_crit : Un_growing -> bound EUn -> exists l : R, Un_cv l.
proof: Proof. intros Hug Heub. exists (proj1_sig (completeness EUn Heub EUn_noempty)). destruct (completeness EUn Heub EUn_noempty) as (l, H). now apply Un_cv_crit_lub. Qed.
imports: Rbase Rfunctions Compare