fact: Definition apart0 xi : bool := match I.sign_strict xi with | Xlt | Xgt => true | _ => false end.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor