fact: Parameter upper_bounded_correct : forall xi, upper_bounded xi = true -> F.convert (upper xi) = Xreal (proj_val (F.convert (upper xi))) /\ bounded_prop xi.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic