proposition: Lemma min_cv : forall (Un:nat -> R) (pr:Cauchy_crit Un), { l:R | Un_cv (sequence_lb Un (cauchy_min Un pr)) l }.
proof: Proof. intros. apply growing_cv. - apply Vn_growing. - apply min_maj. apply cauchy_maj. assumption. Qed.
imports: Rbase Rfunctions Rseries Lia