proposition: Lemma pow_contains_0 (X : I.type) (n : Z) : (n > 0)%Z -> contains (I.convert X) (Xreal 0) -> contains (I.convert (I.power_int prec X n)) (Xreal 0).
proof: Proof. move=> Hn HX. rewrite (_: (Xreal 0) = (Xpower_int (Xreal 0) n)); first exact: I.power_int_correct. case: n Hn =>//= p Hp; rewrite pow_ne_zero //. by zify; auto with zarith. Qed.
imports: Coq(ZArith Reals Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat bigop) Coquelicot(Coquelicot) Stdlib MathComp Xreal Interval Taylor