fact: Definition contains i v := match i, v with | Ibnd l u, Xreal x => match l with | Xreal r => Rle r x | Xnan => True end /\ match u with | Xreal r => Rle x r | Xnan => True end | Inan, _ => True | _, Xnan => False end.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic