proposition: Theorem power_int_correct : forall (p : Z) u (Y : I.type) tf f, approximates Y tf f -> approximates Y (power_int p u Y tf) (fun x => Xbind (fun y => Xpower_int (Xreal y) p) (f x)).
proof: Proof. move=> p u Y tf f Hmain. have [Hp|Hp] := Z.eq_dec p 1%Z. rewrite Hp. apply (@approximates_ext f)=>//. move=> x; rewrite /Xinv. case: (f x) =>[//|r]. by rewrite /= Rmult_1_r. case: p Hp =>[|p'|p']=>//; (try case: p'=>[p''|p''|]) =>// H; apply: (fun_gen_correct (fi := fun prec x => I.power_int prec x _) (ftm := fun prec => TM_power_int prec _) (fx := fun x => Xpower_int (Xreal x) _)) =>//; try (by move=> *; apply: I.power_int_correct); try (by move=> *; rewrite /tmsize size_TM_power_int); by move=> *; apply: TM_power_int_correct. Qed.
imports: Coq(Reals ZArith Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq bigop) Interval Xreal Basic Interval_compl Datatypes Taylor_model_sharp Bound Bound_quad Univariate_sig