fact: Definition subset xi yi := if is_empty xi then true else match xi, yi with | Ibnd xl xu, Ibnd yl yu => match F.cmp xl yl with | Xund => match F.classify yl with | Fnan | Fminfty => true | Freal | Fpinfty => false end | Xlt => false | _ => true end && match F.cmp xu yu with | Xund => match F.classify yu with | Fnan | Fpinfty => true | Freal | Fminfty => false end | Xgt => false | _ => true end | _, Inan => true | Inan, Ibnd _ _ => false end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval