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