proposition: Lemma dicho_up_cv : forall (x y:R) (P:R -> bool), x <= y -> { l:R | Un_cv (dicho_up x y P) l }.
proof: Proof. intros. apply decreasing_cv. - apply dicho_up_decreasing; assumption. - apply dicho_up_min; assumption. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra