proposition: Lemma apart0_correct X x : contains (I.convert X) (Xreal x) -> apart0 X -> (x <> 0)%R.
proof: Proof. move=> Hx; rewrite /apart0. have := I.sign_strict_correct X; case: I.sign_strict=>//; by case/(_ _ Hx) =>/=; auto with real. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor