fact: Definition sqrt prec xi := match xi with | Ibnd xl xu => match F.cmp xl F.zero with | Xgt => Ibnd (F.sqrt_DN prec xl) (F.sqrt_UP prec xu) | _ => Ibnd F.zero (F.sqrt_UP prec xu) end | Inan => Inan end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval