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