fact: Definition join xi yi := if is_empty xi then yi else if is_empty yi then xi else match xi, yi with | Ibnd xl xu, Ibnd yl yu => Ibnd (F.min xl yl) (F.max xu yu) | _, _ => Inan end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval