proposition: Lemma dicho_lb_dicho_up : forall (x y:R) (P:R -> bool) (n:nat), x <= y -> dicho_up x y P n - dicho_lb x y P n = (y - x) / 2 ^ n.
proof: Proof. intros. induction n as [| n Hrecn]. - simpl. unfold Rdiv; rewrite Rinv_1; ring. - simpl. case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)). + unfold Rdiv. replace ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) * / 2 - Dichotomy_lb x y P n) with ((dicho_up x y P n - dicho_lb x y P n) / 2). * unfold Rdiv; rewrite Hrecn. unfold Rdiv. field. apply pow_nonzero; discrR. * pattern (Dichotomy_lb x y P n) at 2; rewrite <-(Rplus_half_diag (Dichotomy_lb x y P n)); unfold dicho_up, dicho_lb, Rminus, Rdiv; ring. + replace (Dichotomy_ub x y P n - (Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2) with ((dicho_up x y P n - dicho_lb x y P n) / 2). * unfold Rdiv; rewrite Hrecn. field. apply pow_nonzero; discrR. * pattern (Dichotomy_ub x y P n) at 1; rewrite <-(Rplus_half_diag (Dichotomy_ub x y P n)); unfold dicho_up, dicho_lb, Rminus, Rdiv; ring. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra