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