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