proposition: Lemma dicho_lb_maj : forall (x y:R) (P:R -> bool), x <= y -> has_ub (dicho_lb x y P).
proof: Proof. intros. cut (forall n:nat, dicho_lb x y P n <= y). - intro. unfold has_ub. unfold bound. exists y. unfold is_upper_bound. intros. elim H1; intros. rewrite H2; apply H0. - apply dicho_lb_maj_y; assumption. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra