fact: Parameter upper_extent_correct : forall xi x y, contains (convert xi) (Xreal y) -> (y <= x)%R -> contains (convert (upper_extent xi)) (Xreal x).
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic