proposition: Lemma dicho_lb_growing : forall (x y:R) (P:R -> bool), x <= y -> Un_growing (dicho_lb x y P).
proof: Proof. intros. unfold Un_growing. intro. simpl. case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)). - right; reflexivity. - unfold Rdiv; apply Rmult_le_reg_l with 2. + prove_sup0. + pattern 2 at 1; rewrite Rmult_comm. rewrite Rmult_assoc; rewrite Rinv_l; [ idtac | discrR ]. rewrite Rmult_1_r. rewrite <-Rplus_diag. apply Rplus_le_compat_l. replace (Dichotomy_ub x y P n) with (dicho_up x y P n); [ apply dicho_comp; assumption | reflexivity ]. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra