proposition: Lemma growing_cv : forall Un:nat -> R, Un_growing Un -> has_ub Un -> { l:R | Un_cv Un l }.
proof: Proof. intros Un Hug Heub. exists (proj1_sig (completeness (EUn Un) Heub (EUn_noempty Un))). destruct (completeness _ Heub (EUn_noempty Un)) as (l, H). now apply Un_cv_crit_lub. Qed.
imports: Rbase Rfunctions Rseries Lia