proposition: Lemma dicho_up_car : forall (x y:R) (P:R -> bool) (n:nat), P y = true -> P (dicho_up x y P n) = true.
proof: Proof. intros. induction n as [| n Hrecn]. - assumption. - simpl. destruct (sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))) as [Heq|Heq]. + rewrite Heq. unfold dicho_lb in Hrecn; assumption. + rewrite Heq. assumption. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra