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