proposition: Lemma isNNegOrNPos_false (X : I.type) : I.convert X = IInan -> isNNegOrNPos X = false.
proof: Proof. move=> H; rewrite /isNNegOrNPos; have := I.sign_large_correct X. by case: I.sign_large =>//; rewrite H; move/(_ Xnan I) =>//; case. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor