proposition: Lemma maj_cv : forall (Un:nat -> R) (pr:Cauchy_crit Un), { l:R | Un_cv (sequence_ub Un (cauchy_maj Un pr)) l }.
proof: Proof. intros. apply decreasing_cv. - apply Wn_decreasing. - apply maj_min. apply cauchy_min. assumption. Qed.
imports: Rbase Rfunctions Rseries Lia