fact: Definition contains_output xi x := match xi with | (None, None) => True | (None, Some xu) => (x <= convert_bound xu)%R | (Some xl, None) => (convert_bound xl <= x)%R | (Some xl, Some xu) => (convert_bound xl <= x <= convert_bound xu)%R end.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic