proposition: Lemma toR_power_int p x : (0 <= p)%Z \/ x <> R0 -> powerRZ x p = proj_val (Xpower_int' x p).
proof: Proof. case => [Hp|Hx]. by case: p Hp =>// p []. by case: p =>//; rewrite /Xpower_int' is_zero_false. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound