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