fact: Parameter midpoint_correct : forall xi, not_empty (convert xi) -> F.convert (midpoint xi) = Xreal (proj_val (F.convert (midpoint xi))) /\ contains (convert xi) (F.convert (midpoint xi)).
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic