proposition: Lemma dicho_comp : forall (x y:R) (P:R -> bool) (n:nat), x <= y -> dicho_lb x y P n <= dicho_up x y P n.
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)). + 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. assumption. + 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. rewrite <- (Rplus_comm (Dichotomy_ub x y P n)). apply Rplus_le_compat_l. assumption. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra