fact: Parameter midpoint_correct : forall x y, sensible_format = true -> real x = true -> real y = true -> (toR x <= toR y)%R -> real (midpoint x y) = true /\ (toR x <= toR (midpoint x y) <= toR y)%R.
imports: Coq(ZArith Reals) Flocq(Zaux Raux) Xreal Basic