proposition: Lemma dicho_lb_maj_y : forall (x y:R) (P:R -> bool), x <= y -> forall n:nat, dicho_lb x y P n <= y.
proof: Proof. intros. induction n as [| n Hrecn]. - simpl; assumption. - simpl. case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)). + assumption. + unfold Rdiv; apply Rmult_le_reg_l with 2. * prove_sup0. * rewrite Rmult_comm. rewrite Rmult_assoc; rewrite Rinv_l; [ rewrite Rmult_1_r | discrR ]. rewrite <-Rplus_diag; apply Rplus_le_compat. -- assumption. -- pattern y at 2; replace y with (Dichotomy_ub x y P 0); [ idtac | reflexivity ]. apply decreasing_prop. ++ assert (H0 := dicho_up_decreasing x y P H). assumption. ++ apply Nat.le_0_l. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra