proposition: Lemma powerRZ_opp x n : x <> 0%R -> powerRZ x (- n) = / (powerRZ x n).
proof: Proof. move=> Hx. case: n =>[|p|p] //; first by rewrite Rinv_1. rewrite Rinv_involutive //. exact: pow_nonzero. 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