proposition: Lemma dicho_lb_cv : forall (x y:R) (P:R -> bool), x <= y -> { l:R | Un_cv (dicho_lb x y P) l }.
proof: Proof. intros. apply growing_cv. - apply dicho_lb_growing; assumption. - apply dicho_lb_maj; assumption. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra