fact: Parameter bisect_correct : forall xi x, contains (convert xi) x -> contains (convert (fst (bisect xi))) x \/ contains (convert (snd (bisect xi))) x.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic