fact: Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := match N with | O => x | S n => let down := Dichotomy_lb x y P n in let up := Dichotomy_ub x y P n in let z := (down + up) / 2 in if P z then down else z end with Dichotomy_ub (x y:R) (P:R -> bool) (N:nat) {struct N} : R := match N with | O => y | S n => let down := Dichotomy_lb x y P n in let up := Dichotomy_ub x y P n in let z := (down + up) / 2 in if P z then z else up end.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra