proposition: Lemma toR_power_int_loc p x : (0 <= p)%Z \/ x <> R0 -> locally x (fun t => powerRZ t p = proj_val (Xpower_int' t p)).
proof: Proof. case: p => [|p|p] Hx. - eapply (locally_open (fun _ => True)) =>//; exact: open_true. - eapply (locally_open (fun _ => True)) =>//; exact: open_true. - eapply (@locally_open _ (fun x => x <> 0)%R) =>//; first exact: open_neq. by move => {x Hx} x Hx; rewrite /= is_zero_false. case: Hx => // ; by case. 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