proposition: Lemma pow_Rabs_sign (r : R) (n : nat) : (r ^ n = powerRZ (if Rle_bool R0 r then 1 else -1) (Z_of_nat n) * (Rabs r) ^ n)%R.
proof: Proof. elim: n =>[|n /= ->]; first by rewrite Rmult_1_l. case: Rle_bool_spec => Hr. rewrite powerRZ_R1 Rmult_1_l SuccNat2Pos.id_succ. by rewrite pow1 Rabs_pos_eq // Rmult_1_l. by rewrite {-1 3}Rabs_left // SuccNat2Pos.id_succ -pow_powerRZ /=; ring. 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