fact: Definition sign_large_ xl xu := match F.cmp xl F.zero, F.cmp xu F.zero with | Xeq, Xeq => Xeq | _, Xlt => Xlt | _, Xeq => Xlt | Xgt, _ => Xgt | Xeq, _ => Xgt | _, _ => Xund end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval